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

rho_of_subgroup

PFR.RhoFunctional · PFR/RhoFunctional.lean:679 to 725

Source documentation

If $H$ is a finite subgroup of $G$ , and $\rho(U_H) \leq r$ , then there exists $t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$ , and $|H|/|A| \in [e^{-2r}, e^{2r}]$ .

Exact Lean statement

lemma rho_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G}
    (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U)
    (r : ℝ) (hr : ρ[U ; μ # A] ≤ r) :
    ∃ t : G,
      exp (-r) * Nat.card A ^ (1/2 : ℝ) * (H : Set G).ncard ^ (1/2 : ℝ) ≤
        Nat.card ↑(↑A ∩ (t +ᵥ (H : Set G)))
      ∧ Nat.card A ≤ exp (2 * r) * (H : Set G).ncard
      ∧ (H : Set G).ncard ≤ exp (2 * r) * Nat.card A

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rho_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G}    (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U)    (r : ℝ) (hr : ρ[U ; μ # A] ≤ r) :    ∃ t : G,      exp (-r) * Nat.card A ^ (1/2 : ℝ) * (H : Set G).ncard ^ (1/2 : ℝ) ≤        Nat.card ↑(↑A ∩ (t +ᵥ (H : Set G)))      ∧ Nat.card A ≤ exp (2 * r) * (H : Set G).ncard      ∧ (H : Set G).ncard ≤ exp (2 * r) * Nat.card A := by  have hr' : ρ[U ; μ # A] ≤ r := hr  have Hpos : 0 < ((H : Set G).ncard : ℝ) := by exact_mod_cast Nat.card_pos  have : Nonempty A := hA.to_subtype  have Apos : 0 < (Nat.card A : ℝ) := by exact_mod_cast Nat.card_pos  simp only [rho] at hr  rw [rhoMinus_of_subgroup hunif hA hU, rhoPlus_of_subgroup hunif hA hU] at hr  rcases exists_card_inter_add_eq_sSup (A := A) H hA with ⟨t, ht, hpos⟩  rw [← ht] at hr  have Rm : 0 ≤ ρ⁻[U ; μ # A] := rhoMinus_nonneg hU  have RM : 0 ≤ ρ⁺[U ; μ # A] := by    rw [rhoPlus_of_subgroup hunif hA hU, ← ht, sub_nonneg]    apply log_le_log (mod_cast hpos)    norm_cast    have : Nat.card (t +ᵥ (H : Set G) : Set G) = (H : Set G).ncard := by      apply Nat.card_image_of_injective (add_right_injective t)    rw [← this]    exact Nat.card_mono (toFinite _) inter_subset_right  have I : |log ((H : Set G).ncard) - log (Nat.card A)| ≤ 2 * r := calc    |log ((H : Set G).ncard) - log (Nat.card A)|    _ = |H[U ; μ] - log (Nat.card A)| := by rw [hunif.entropy_eq' (toFinite _) hU]    _ = |ρ⁺[U ; μ # A] - ρ⁻[U ; μ # A]| := by congr 1; simp [rhoPlus]; abel    _ ≤ ρ⁺[U ; μ # A] + ρ⁻[U ; μ # A] :=      (abs_sub _ _).trans_eq (by simp [abs_of_nonneg, Rm, RM])    _ = 2 * ρ[U ; μ # A] := by simp [rho]; ring    _ ≤ 2 * r := by linarith  refine ⟨t, ?_, ?_, ?_⟩  · have : - r + (log (Nat.card A) + log ((H : Set G).ncard)) * (1 / 2 : ℝ) ≤      log (Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G)) := by linarith    have := exp_monotone this    rwa [exp_add, exp_log (mod_cast hpos), exp_mul, exp_add,      exp_log Hpos, exp_log Apos, mul_rpow, ← mul_assoc] at this <;> positivity  · have : log (Nat.card A) ≤ 2 * r + log ((H : Set G).ncard) := by      linarith [(abs_sub_le_iff.1 I).2]    have := exp_monotone this    rwa [exp_log Apos, exp_add, exp_log Hpos] at this  · have : log ((H : Set G).ncard) ≤ 2 * r + log (Nat.card A) := by      linarith [(abs_sub_le_iff.1 I).1]    have := exp_monotone this    rwa [exp_log Hpos, exp_add, exp_log Apos] at this