Documentation

Lean 4 Proof

theorem knockout_partial_retained {ρ : ℝ} (hρ : 0 < ρ) {m : ℕ}
    (_hJ : 0 < J) (_hm_pos : 0 < m) (_hm_lt : m < J) :
    0 < knockoutRetained J ρ m ∧ knockoutRetained J ρ m < 1 := by
  simp only [knockoutRetained, show ρ > 0 from hρ, if_true]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast _hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  -- Key: 0 < (J-m)/J < 1
  have hmJ : (↑m : ℝ) < ↑J := by exact_mod_cast _hm_lt
  have hJm_pos : (0 : ℝ) < ↑J - ↑m := by linarith
  have hfrac_pos : (0 : ℝ) < (↑J - ↑m) / ↑J := div_pos hJm_pos hJpos
  have hfrac_lt : (↑J - ↑m) / (↑J : ℝ) < 1 := by
    rw [div_lt_one hJpos]; linarith [show (0 : ℝ) < ↑m from by exact_mod_cast _hm_pos]
  have hexp_pos : (0 : ℝ) < 1 / ρ := div_pos one_pos hρ
  constructor
  · exact rpow_pos_of_pos hfrac_pos _
  · exact rpow_lt_one (le_of_lt hfrac_pos) hfrac_lt hexp_pos

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:66

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file