theorem proved tactic proof

`anomalous_nu_correction_small`

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

formal statement (Lean)

 147theorem anomalous_nu_correction_small (D η : ℝ) (hD : 0 < D) (hη : 0 ≤ η) :
 148    anomalous_nu_correction D η ≤ η / D := by

proof body

Tactic-mode proof.

 149  unfold anomalous_nu_correction
 150  have hDη : 0 < D + η := by linarith
 151  have hDη_ne : D + η ≠ 0 := ne_of_gt hDη
 152  have hD_ne : D ≠ 0 := ne_of_gt hD
 153  rcases eq_or_lt_of_le hη with rfl | hη_pos
 154  · simp
 155  · rw [div_le_div_iff₀ hDη hD]
 156    nlinarith
 157
 158/-- The corrected ν₀ + η/(D + η). -/

depends on (1)

Lean names referenced from this declaration's body.

anomalous_nu_correction in IndisputableMonolith.Physics.ThermalFixedPoint decl_use