Unbalancing

theorem pow_inner_nonneg' {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {ν : G → NNReal} {g h f : G → ℂ} (hf : g ○ᵈ g = f) (hν : h ○ᵈ h = (fun (x : NNReal) => ↑↑x) ∘ ν) (k : ℕ) : 0 ≤ ⟪f ^ k, (fun (x : NNReal) => ↑↑x) ∘ ν⟫_[ℂ]

Note that we do the physical proof in order to avoid the Fourier transform.

theorem pow_inner_nonneg {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] {ν : G → NNReal} {g h : G → ℂ} {f : G → ℝ} (hf : g ○ᵈ g = Complex.ofReal ∘ f) (hν : h ○ᵈ h = (fun (x : NNReal) => ↑↑x) ∘ ν) (k : ℕ) : 0 ≤ ⟪NNReal.toReal ∘ ν, f ^ k⟫_[ℝ]

Note that we do the physical proof in order to avoid the Fourier transform.

theorem unbalancing' {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (ν : G → NNReal) (f : G → ℝ) (g h : G → ℂ) (hf : g ○ᵈ g = Complex.ofReal ∘ f) (hν : h ○ᵈ h = (fun (x : NNReal) => ↑↑x) ∘ ν) (hν₁ : ∑ x : G, ν x = 1) (hε : ε ≤ ‖f‖_[↑p, ν]) : ∃ (p' : ℕ), ↑p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * ↑p ∧ 1 + ε / 2 ≤ ‖f + 1‖_[↑p', ν]

The unbalancing step. Note that we do the physical proof in order to avoid the Fourier transform.

theorem unbalancing {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (f : G → ℝ) (g h : G → ℂ) (hf : g ○ᵈ g = Complex.ofReal ∘ f) (hh : h ○ᵈ h = mu Finset.univ) (hε : ε ≤ ‖f‖_[↑p, mu Finset.univ]) : ∃ (p' : ℕ), ↑p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * ↑p ∧ 1 + ε / 2 ≤ ‖f + 1‖_[↑p', mu Finset.univ]

The unbalancing step. Note that we do the physical proof in order to avoid the Fourier transform.