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

is_tau_min

PFR.TauFunctional · PFR/TauFunctional.lean:170 to 177

Mathematical statement

Exact Lean statement

lemma is_tau_min (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') :
    τ[X₁ # X₂ | p] ≤ τ[X₁' # X₂' | p]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma is_tau_min (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂') :    τ[X₁ # X₂ | p] ≤ τ[X₁' # X₂' | p] := by  let ν₁ := (ℙ : Measure Ω'₁).map X₁'  let ν₂ := (ℙ : Measure Ω'₂).map X₂'  have B : τ[X₁' # X₂' | p] = τ[id ; ν₁ # id ; ν₂ | p] :=    (identDistrib_id_right h1.aemeasurable).tau_eq p (identDistrib_id_right h2.aemeasurable)  convert h ν₁ ν₂ (Measure.isProbabilityMeasure_map h1.aemeasurable)    (Measure.isProbabilityMeasure_map h2.aemeasurable)