Documentation

Lean 4 Proof

theorem bridgeRatio_large_at_small_rho {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1)
    (hM : 0 < M) (hρM : ρ < 1 / (M + 1)) :
    M < bridgeRatio ρ := by
  have hρ2 : 0 < ρ ^ 2 := sq_pos_of_pos hρ
  rw [bridgeRatio, lt_div_iff₀ hρ2]
  -- Need: M · ρ² < 1 - ρ, i.e., ρ(M+1) < 1 and ρ² ≤ ρ
  have h1 : ρ ^ 2 ≤ ρ := by
    rw [sq]; exact mul_le_of_le_one_left hρ.le hρ1.le
  have h2 : ρ * (M + 1) < 1 := by
    rwa [lt_div_iff₀ (by linarith : (0 : ℝ) < M + 1)] at hρM
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:378

Module Section

Information Geometry of CES:

In the same file