Source indexedtheorem · leanprover/lean4:v4.33.0-rc1

tau_strictly_decreases'

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:700 to 708

Mathematical statement

Exact Lean statement

theorem tau_strictly_decreases' (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tau_strictly_decreases' (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0 := by  let ⟨A, mA, μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩    := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ  rw [← h_id1.rdist_congr h_id2]  let _ : MeasureSpace A := ⟨μ⟩  have : IsProbabilityMeasure (ℙ : Measure A) := hμ  rw [← h_id1.tau_minimizes p h_id2] at h_min  exact tau_strictly_decreases_aux' p hY₁ hY₂ hY₁' hY₂' (h_id1.trans h_id1'.symm)    (h_id2.trans h_id2'.symm) h_indep.reindex_four_abdc h_min hp