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

sub_multiDistance_le

PFR.MultiTauFunctional · PFR/MultiTauFunctional.lean:203 to 223

Source documentation

If $(X_i)_{1 \leq i \leq m}$ is a $\tau$ -minimizer, and $k := D[(X_i)_{1 \leq i \leq m}]$ , then for any other tuple $(X'_i)_{1 \leq i \leq m}$ , one has $k - D[(X'_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i].$

Exact Lean statement

lemma sub_multiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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)) :
    D[X; hΩ] - D[X'; hΩ'] ≤ p.η * ∑ i, d[X i ; (hΩ i).volume # X' i; (hΩ' i).volume ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sub_multiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [hΩ₀ : 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)) :    D[X; hΩ] - D[X'; hΩ'] ≤ p.η * ∑ i, d[X i ; (hΩ i).volume # X' i; (hΩ' i).volume ] := by  suffices D[X; hΩ] + p.η * ∑ i, d[X i ; (hΩ i).volume # p.X₀; hΩ₀.volume ]      ≤ D[X'; hΩ'] + (p.η * ∑ i, d[X i ; (hΩ i).volume # p.X₀; hΩ₀.volume ]        + p.η * ∑ i, d[X i ; (hΩ i).volume # X' i; (hΩ' i).volume ]) by linarith  calc    _ ≤ D[X'; hΩ'] + p.η * ∑ i, d[X' i ; (hΩ' i).volume # p.X₀; hΩ₀.volume ] :=      h_min Ω' hΩ' hΩprob' X' hmeasX'    _ ≤ _ := by      have hη : p.η > 0 := p.hη      have hprob := p.hprob      rw [←  mul_add, ← Finset.sum_add_distrib]      gcongr with i _      rw [add_comm, rdist_symm (Y := X' i)]      apply rdist_triangle (hmeasX' i) (hmeasX i) p.hmeas