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

rdist_le_of_isUniform_of_card_add_le

PFR.Main · PFR/Main.lean:113 to 132

Source documentation

A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

Exact Lean statement

theorem rdist_le_of_isUniform_of_card_add_le [A_fin : Finite A] [MeasurableSpace G]
    [MeasurableSingletonClass G]
    (hA₀ : A.Nonempty) (hA : (A - A).ncard ≤ K * A.ncard)
    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rdist_le_of_isUniform_of_card_add_le [A_fin : Finite A] [MeasurableSpace G]    [MeasurableSingletonClass G]    (hA₀ : A.Nonempty) (hA : (A - A).ncard ≤ K * A.ncard)    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K := by  obtain ⟨A_pos, AA_pos, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A - A).ncard ∧ 0 < K :=    PFR_conjecture_pos_aux A.toFinite hA₀ hA  rcases independent_copies_two U₀meas U₀meas with ⟨Ω, mΩ, U, U', hP, hU, hU', UU'_indep, idU, idU'⟩  have Uunif : IsUniform A U := U₀unif.of_identDistrib idU.symm .of_discrete  have U'unif : IsUniform A U' := U₀unif.of_identDistrib idU'.symm .of_discrete  have IU : d[U # U'] ≤ log K := by    have I : H[U - U'] ≤ log (A - A).ncard := by      apply entropy_le_log_card_of_mem_finite (Set.Finite.sub A_fin A_fin) (hU.sub hU')      filter_upwards [Uunif.ae_mem, U'unif.ae_mem] with ω h1 h2      exact Set.sub_mem_sub h1 h2    have J : log (A - A).ncard ≤ log K + log A.ncard := by      rw [← log_mul K_pos.ne' A_pos.ne']; gcongr    rw [UU'_indep.rdist_eq hU hU', Uunif.entropy_eq' A_fin hU, U'unif.entropy_eq' A_fin hU']    linarith  rwa [idU.rdist_congr idU'] at IU