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

rhoMinus_of_subgroup

PFR.RhoFunctional · PFR/RhoFunctional.lean:631 to 639

Source documentation

If $H$ is a finite subgroup of $G$ , then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$ .

Exact Lean statement

lemma rhoMinus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G}
    {U : Ω → G} (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) :
    ρ⁻[U ; μ # A] = log (Nat.card A) -
      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rhoMinus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G}    {U : Ω → G} (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) :    ρ⁻[U ; μ # A] = log (Nat.card A) -      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ) := by  apply le_antisymm _ (le_rhoMinus_of_subgroup hunif hA hU)  rcases exists_card_inter_add_eq_sSup (A := A) H hA with ⟨t, ht, hpos⟩  rw [← ht]  have : Nonempty (A ∩ (t +ᵥ (H : Set G)) : Set G) :=  (Nat.card_pos_iff.1 hpos).1  exact rhoMinus_le_of_subgroup t hunif hA .of_subtype hU