PhaseGiantMean.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The positive uniform-support mean of the Fourier-phase giant

theorem OAI.Ostmann.densityFourier_reflect line 10
theorem OAI.Ostmann.densityFourier_twice line 14
theorem OAI.Ostmann.densityFourier_inverse line 25
theorem OAI.Ostmann.phaseGiantPhysical_transform line 32
Source documentation
The giant's Fourier transform is exactly the bounded phase specified in Section 7.1, not merely an energy majorant.
```
theorem phaseGiantPhysical_transform {p : ℕ} [NeZero p] (g : ZMod p → ℂ) (b : ZMod p) :
    densityFourier (phaseGiantPhysical g) b = complexUnitPhase (g b) :=
…
```
Mentions: OAI.Ostmann.densityFourier, OAI.Ostmann.phaseGiantPhysical, OAI.Ostmann.complexUnitPhase
theorem OAI.Ostmann.densityFourierInverse_sum line 36
theorem OAI.Ostmann.phaseGiantPhysical_sum_zero line 46

theorem OAI.Ostmann.phaseGiantPhysical_support_sum line 51

Source documentation

Exact support sum before converting it to a uniform mean.

theorem phaseGiantPhysical_support_sum {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p) :
    (∑ x ∈ S, phaseGiantPhysical (normalizedResidueTransform S) x) =
      (Real.sqrt (residueVariance S) : ℂ) *
        ((∑ b, ‖normalizedResidueTransform S b‖ : ℝ) : ℂ) := by
…

Mentions: OAI.Ostmann.phaseGiantPhysical, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.residueVariance

theorem OAI.Ostmann.phaseGiantPhysical_uniform_mean_lower line 78

Source documentation

A fixed positive fraction of the Fourier L1 mean survives on the actual residue support. The relaxed constant one half is sufficient downstream.

theorem phaseGiantPhysical_uniform_mean_lower {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p)
    (hσ : residueDensity S ≤ 2 / 3) :
    (1 / 2 : ℝ) * ((p : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform S b‖) ≤
      (S.card : ℝ)⁻¹ * ∑ x ∈ S, (phaseGiantPhysical (normalizedResidueTransform S) x).re := by
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.phaseGiantPhysical