pith. machine review for the scientific record. sign in
theorem proved tactic proof

predictability_threshold_band

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  65theorem predictability_threshold_band :
  66    0.11 < PredictabilityThreshold ∧ PredictabilityThreshold < 0.13 := by

proof body

Tactic-mode proof.

  67  unfold PredictabilityThreshold
  68  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  69  rw [Cost.Jcost_eq_sq hphi_ne]
  70  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  71  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  72  have hpos : (0 : ℝ) < 2 * phi := by
  73    have : (0 : ℝ) < phi := Constants.phi_pos
  74    linarith
  75  refine ⟨?lo, ?hi⟩
  76  · rw [lt_div_iff₀ hpos]
  77    nlinarith [h_lo, h_hi]
  78  · rw [div_lt_iff₀ hpos]
  79    nlinarith [h_lo, h_hi]
  80

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.