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

tau_strictly_decreases

PFR.EntropyPFR · PFR/EntropyPFR.lean:38 to 48

Source documentation

If $d[X_1;X_2] > 0$ then there are $G$ -valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$ . Phrased in the contrapositive form for convenience of proof.

Exact Lean statement

theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1 / 9) :
    d[X₁ # X₂] = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1 / 9) :    d[X₁ # X₂] = 0 := by  cases nonempty_fintype G  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  apply tau_strictly_decreases_aux p Y₁ Y₂ Y₁' Y₂' hY₁ hY₂ hY₁' hY₂' (h_id1.trans h_id1'.symm)    (h_id2.trans h_id2'.symm) h_indep h_min hpη