Chang's lemma

noncomputable def changConst : ℝ

Equations

• changConst = 32 * Real.exp 1

theorem one_lt_changConst : 1 < changConst

theorem changConst_pos : 0 < changConst

def Mathlib.Meta.Positivity.evalChangConst : PositivityExt

Extension for the positivity tactic: changConst is positive.

Equations

• One or more equations did not get rendered due to their size.

theorem AddDissociated.boringEnergy_le {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] [DecidableEq G] [Finite G] {s : Finset G} (hs : AddDissociated ↑s) (n : ℕ) : boringEnergy n s ≤ changConst ^ n * ↑n ^ n * ↑s.card ^ n

theorem general_hoelder {G : Type u_1} [AddCommGroup G] {f : G → ℂ} {η : ℝ} {Δ : Finset (AddChar G ℂ)} {m : ℕ} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hη : 0 ≤ η) (ν : G → NNReal) (hfν : ∀ (x : G), f x ≠ 0 → 1 ≤ ν x) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) : ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤ energy m Δ (dft fun (a : G) => ↑↑(ν a))

theorem spec_hoelder {G : Type u_1} [AddCommGroup G] {f : G → ℂ} {η : ℝ} {Δ : Finset (AddChar G ℂ)} {m : ℕ} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) : ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / ↑(Fintype.card G))) ≤ boringEnergy m Δ

theorem chang {G : Type u_1} [AddCommGroup G] {f : G → ℂ} {η : ℝ} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hf : f ≠ 0) (hη : 0 < η) : ∃ Δ ⊆ largeSpec f η, Δ.card ≤ ⌈changConst * Real.exp 1 * ↑⌈1 + Real.log (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / ↑(Fintype.card G))⁻¹⌉₊ / η ^ 2⌉₊ ∧ largeSpec f η ⊆ Δ.addSpan

Chang's lemma.