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

iter_multiDist_chainRule

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:2016 to 2059

Source documentation

Let m be a positive integer. Suppose one has a sequence G_m → G_{m - 1} → ... → G_1 → G_0 = {0} of homomorphisms between abelian groups G_0, ...,G_m, and for each d=0, ...,m, let π_d : G_m → G_d be the homomorphism from G_m to G_d arising from this sequence by composition (so for instance π_m is the identity homomorphism and π_0 is the zero homomorphism). Let X_[m] = (X_1, ..., X_m) be a jointly independent tuple of G_m-valued random variables. Then D[X_[m]] = ∑ d, D[π_d(X_[m]) ,| , π_(d-1)(X_[m])] + ∑_{d=1}^{m - 1}, I[∑ i, X_i : π_d(X_[m]) | π_d(∑ i, X_i), π_(d-1})(X_[m])].

Exact Lean statement

lemma iter_multiDist_chainRule {m : ℕ}
    {G : Fin (m + 1) → Type*}
    [hG : ∀ i, MeasurableSpace (G i)] [hGs : ∀ i, MeasurableSingletonClass (G i)]
    [∀ i, AddCommGroup (G i)] [hGcount : ∀ i, Fintype (G i)]
    {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc} {π : ∀ d, G ⊤ →+ G d}
    (hcomp: ∀ i : Fin m, π i.castSucc = (φ i) ∘ (π i.succ))
    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → G ⊤}
    (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) (n : Fin (m + 1)) :
    D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ] = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]
      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |
            ⟨(π (d+1)) ∘ ∑ i, X i, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma iter_multiDist_chainRule {m : ℕ}    {G : Fin (m + 1) → Type*}    [hG : ∀ i, MeasurableSpace (G i)] [hGs : ∀ i, MeasurableSingletonClass (G i)]    [∀ i, AddCommGroup (G i)] [hGcount : ∀ i, Fintype (G i)]    {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc} {π : ∀ d, G ⊤ →+ G d}    (hcomp: ∀ i : Fin m, π i.castSucc = (φ i) ∘ (π i.succ))    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → G ⊤}    (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) (n : Fin (m + 1)) :    D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ] = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]      + I[∑ i, X i : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |            ⟨(π (d+1)) ∘ ∑ i, X i, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩]) := by  set S := ∑ i, X i  set motive := fun n:Fin (m + 1) ↦ D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ]    = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]      + I[S : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |            ⟨(π (d+1)) ∘ S, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩])  have zero : motive 0 := by    have : (Finset.Iio 0 : Finset (Fin (m + 1))) = ∅ := rfl    simp [motive, this]  have succ : (n : Fin m) → motive n.castSucc → motive n.succ := by    intro n hn    dsimp [motive] at hn ⊢    have h2 : n.castSucc ∈ Finset.Iio n.succ := by simp [Fin.castSucc_lt_succ_iff]    rw [hn, ← Finset.add_sum_erase _ _ h2, Fin.Iio_succ_eq_Iic_castSucc, Finset.Iic_erase,      ← add_assoc, ← add_assoc, Fin.coeSucc_eq_succ]    congr 1    convert! cond_multiDist_chainRule (Y := fun i ↦ π n.castSucc ∘ X i) (π n.succ) hX ?_ ?_    · set g : G n.succ → G n.succ × G n.castSucc := fun x ↦ ⟨x, ⇑(φ n) x⟩      convert (condMultiDist_of_inj (f := g) (fun _ ↦ hΩ) X (fun i ↦ ⇑(π n.succ) ∘ X i) _).symm        using 3 with i      · ext ω        · dsimp [g, prod]        rw [hcomp n]        simp [g]      simp [Injective, g]    · intro _      exact Measurable.comp .of_discrete (hX _)    set g : G ⊤ → G ⊤ × G n.castSucc := fun x ↦ ⟨x, π n.castSucc x⟩    convert! h_indep.comp (fun _ ↦ g) _    intro _    exact .of_discrete  exact Fin.induction zero succ n