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

ProbabilityTheory.Kernel.rdist_triangle_aux2

PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:310 to 346

Mathematical statement

Exact Lean statement

lemma rdist_triangle_aux2 (η : Kernel T' G) (ξ : Kernel T'' G)
    [IsMarkovKernel η] [IsMarkovKernel ξ]
    (μ : Measure T) (μ' : Measure T') (μ'' : Measure T'')
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [IsProbabilityMeasure μ'']
    [FiniteSupport μ] [FiniteSupport μ'] [FiniteSupport μ''] :
    Hk[map (prodMkLeft (T × T'') η ×ₖ prodMkRight T' (prodMkLeft T ξ))
      (fun p ↦ p.1 - p.2), (μ.prod μ'').prod μ']
    = Hk[map (prodMkRight T'' η ×ₖ prodMkLeft T' ξ) (fun x ↦ x.1 - x.2), μ'.prod μ'']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_triangle_aux2 (η : Kernel T' G) (ξ : Kernel T'' G)    [IsMarkovKernel η] [IsMarkovKernel ξ]    (μ : Measure T) (μ' : Measure T') (μ'' : Measure T'')    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [IsProbabilityMeasure μ'']    [FiniteSupport μ] [FiniteSupport μ'] [FiniteSupport μ''] :    Hk[map (prodMkLeft (T × T'') η ×ₖ prodMkRight T' (prodMkLeft T ξ))      (fun p ↦ p.1 - p.2), (μ.prod μ'').prod μ']    = Hk[map (prodMkRight T'' η ×ₖ prodMkLeft T' ξ) (fun x ↦ x.1 - x.2), μ'.prod μ''] := by  have hBC :      ∀ᵐ x ∂(μ'.prod μ''), x ∈ ((μ'.support ×ˢ μ''.support : Finset (T' × T'')):Set (T' × T'')) :=    Measure.prod_of_full_measure_finset (measure_compl_support μ') (measure_compl_support μ'')  have hAC: (μ.prod μ'') ((μ.support ×ˢ μ''.support : Finset (T × T'')):Set (T × T''))ᶜ = 0 :=    Measure.prod_of_full_measure_finset (measure_compl_support μ) (measure_compl_support μ'')  have hACB : ∀ᵐ x ∂(μ.prod μ'').prod μ', x ∈      (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))    := Measure.prod_of_full_measure_finset hAC (measure_compl_support μ')  simp_rw [entropy, integral_eq_setIntegral hACB, integral_eq_setIntegral hBC,    setIntegral_finset _ .finset, smul_eq_mul, Measure.prod_real_singleton]  conv_rhs => rw [Finset.sum_product_right]  conv_lhs => rw [Finset.sum_product, Finset.sum_product_right]  simp_rw [mul_assoc, ← Finset.mul_sum]  congr with z  have : ∀ x y, map (prodMkLeft (T × T'') η ×ₖ prodMkRight T' (prodMkLeft T ξ))        (fun p ↦ p.1 - p.2) ((x, z), y)      = map (prodMkLeft T'' η ×ₖ prodMkRight T' ξ) (fun p ↦ p.1 - p.2) (z, y) := by    intro x y    ext s hs    rw [map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ hs, prod_apply, prod_apply]    simp  simp_rw [this, ← Finset.sum_mul, sum_measureReal_singleton, Measure.real,    measure_of_measure_compl_eq_zero (measure_compl_support μ),    measure_univ, ENNReal.toReal_one, one_mul, ← mul_assoc, mul_comm _ (μ'' {z}).toReal, mul_assoc,    ← Finset.mul_sum]  congr with y  congr 2 with s _hs  rw [map_apply _ (by fun_prop), map_apply _ (by fun_prop), prod_apply, prod_apply]  simp