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

sub_condMultiDistance_le'

PFR.MultiTauFunctional · PFR/MultiTauFunctional.lean:342 to 372

Source documentation

With the notation of the previous lemma, we have \begin{equation}\label{5.3-conv} k - D[ X'{[m]} | Y{[m]} ] \leq \eta \sum_{i=1}^m d[X_{\sigma(i)};X'_i|Y_i] \end{equation} for any permutation $\sigma : \{1,\dots,m\} \rightarrow \{1,\dots,m\}$ .

Exact Lean statement

lemma sub_condMultiDistance_le' {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]
    {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : ∀ i, MeasureSpace (Ω i)}
    (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)
    {X : ∀ i, Ω i → G} (hmeasX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X)
    {Ω' : Fin p.m → Type u} {hΩ' : ∀ i, MeasureSpace (Ω' i)}
    (hΩ'prob : ∀ i, IsProbabilityMeasure (hΩ' i).volume) {X' : ∀ i, Ω' i → G}
    (hmeasX' : ∀ i, Measurable (X' i))
    {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]
    {Y : ∀ i, Ω' i → S} (hY : ∀ i, Measurable (Y i)) (φ : Equiv.Perm (Fin p.m)) :
    D[X; hΩ] - D[X'|Y; hΩ'] ≤
      p.η * ∑ i, d[X (φ i) ; (hΩ (φ i)).volume # X' i | Y i; (hΩ' i).volume ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sub_condMultiDistance_le' {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureSpace Ω₀]    {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : ∀ i, MeasureSpace (Ω i)}    (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)    {X : ∀ i, Ω i → G} (hmeasX : ∀ i, Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X)    {Ω' : Fin p.m → Type u} {hΩ' : ∀ i, MeasureSpace (Ω' i)}    (hΩ'prob : ∀ i, IsProbabilityMeasure (hΩ' i).volume) {X' : ∀ i, Ω' i → G}    (hmeasX' : ∀ i, Measurable (X' i))    {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]    {Y : ∀ i, Ω' i → S} (hY : ∀ i, Measurable (Y i)) (φ : Equiv.Perm (Fin p.m)) :    D[X; hΩ] - D[X'|Y; hΩ'] ≤      p.η * ∑ i, d[X (φ i) ; (hΩ (φ i)).volume # X' i | Y i; (hΩ' i).volume ] := by  let Xφ := fun i => X (φ i)  let Ωφ := fun i => Ω (φ i)  let hΩφ := fun i => hΩ (φ i)  let hΩφprob := fun i => hΩprob (φ i)  let hmeasXφ := fun i => hmeasX (φ i)  calc    _ = D[Xφ; hΩφ] - D[X'|Y; hΩ'] := by      congr 1      rw [multiDist_of_perm hΩ hΩprob X φ]    _ ≤ _ := by      apply sub_condMultiDistance_le hΩφprob hmeasXφ _ hΩ'prob hmeasX' hY      intro Ω'' hΩ'' hprob X'' hX''      calc      _ = multiTau p Ω hΩ X := by        dsimp [multiTau]        congr 1        · exact multiDist_of_perm hΩ hΩprob X φ        congr 1        exact Fintype.sum_equiv φ _ _ fun _ ↦ rfl      _ ≤ multiTau p Ω'' hΩ'' X'' := h_min Ω'' hΩ'' hprob X'' hX''