Documentation

Lean 4 Proof

theorem variance_gap_shrinks (S₀ M sig_new : ℝ) (hM : 1 < M) (n : ℕ) :
    |varianceGap S₀ M sig_new (n + 1)| ≤ |varianceGap S₀ M sig_new n| := by
  simp only [varianceGap, pow_succ]
  rw [← mul_assoc, abs_mul]
  apply mul_le_of_le_one_right (abs_nonneg _)
  rw [abs_le]
  have hMpos : (0:ℝ) < M := by linarith
  have h1M : 0 < 1 / M := div_pos one_pos hMpos
  have h1Mle : 1 / M ≤ 1 := by rw [div_le_one hMpos]; linarith
  exact ⟨by linarith, by linarith⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:144

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file