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

condMultiDist_of_inj

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1543 to 1564

Source documentation

Conditional multidistance is unchanged if we apply an injection to the conditioned variables

Exact Lean statement

theorem condMultiDist_of_inj {G : Type*} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ}
    {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) {S : Type*} [Fintype S] {T : Type*}
    [Fintype T] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) {f : S → T} (hf : Injective f) :
    D[X | fun i ↦ f ∘ (Y i); hΩ] = D[X | fun i ↦ Y i; hΩ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem condMultiDist_of_inj {G : Type*} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ}    {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) {S : Type*} [Fintype S] {T : Type*}    [Fintype T] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) {f : S → T} (hf : Injective f) :    D[X | fun i ↦ f ∘ (Y i); hΩ] = D[X | fun i ↦ Y i; hΩ] := by  set e : (Fin m → S) → (Fin m → T) := fun y ↦ f ∘ y  convert! (Fintype.sum_of_injective e (Injective.comp_left hf) ?_ ?_ _ _).symm  · intro z hz    convert zero_mul ?_    rw [Finset.prod_eq_zero_iff]    simp only [Set.mem_range, not_exists, e] at hz    contrapose! hz    have : ∀ i, ∃ yi, f yi = z i := by      intro i      replace hz := hz i (Finset.mem_univ i)      contrapose! hz      have : f ∘ Y i ⁻¹' {z i} = ∅ := by aesop      simp [this]    obtain ⟨y, hy⟩ := Classical.axiomOfChoice this    use y    aesop  intro s; congr  all_goals ext; congr; aesop