ThreePrimeContinuousEnergy.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle line 10
def OAI.Problem337.ThreePrimeContinuousEnergy.polynomial line 13
Source documentation
A finite exponential polynomial on the normalized unit circle.
```
def polynomial (s : Finset ℤ) (w : ℤ → ℂ) (x : UnitCircle) : ℂ :=
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle
lemma OAI.Problem337.ThreePrimeContinuousEnergy.continuous_polynomial line 16
lemma OAI.Problem337.ThreePrimeContinuousEnergy.integrable_of_continuous line 21
theorem OAI.Problem337.ThreePrimeContinuousEnergy.integral_fourier_mul_conj line 27
Source documentation
Character orthogonality with the orientation used in a squared norm.
```
theorem integral_fourier_mul_conj (m n : ℤ) :
    (∫ x : UnitCircle, fourier m x * conj (fourier n x)
      ∂AddCircle.haarAddCircle) = if m = n then 1 else 0 := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle
theorem OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_parseval line 35
Source documentation
Exact continuous Parseval for finitely supported Fourier coefficients.
```
theorem polynomial_parseval (s : Finset ℤ) (w : ℤ → ℂ) :
    (∫ x : UnitCircle, ‖polynomial s w x‖ ^ 2 ∂AddCircle.haarAddCircle) =
      ∑ n ∈ s, ‖w n‖ ^ 2 := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle, OAI.Problem337.ThreePrimeContinuousEnergy.polynomial

theorem OAI.Problem337.ThreePrimeContinuousEnergy.cubic_setIntegral_bound line 71

Source documentation

A measure-theoretic cubic minor-set bound. Only the square energy must be integrable; the actual supremum and phase estimates are explicit.

theorem cubic_setIntegral_bound {α : Type*} [MeasurableSpace α]
    (μ : Measure α) (f phase : α → ℂ) (minor : Set α)
    (hmeas : MeasurableSet minor) (B : ℝ) (hB : 0 ≤ B)
    (henergy : Integrable (fun x => ‖f x‖ ^ 2) μ)
    (hminor : ∀ x ∈ minor, ‖f x‖ ≤ B)
    (hphase : ∀ x ∈ minor, ‖phase x‖ ≤ 1) :
    ‖∫ x in minor, f x ^ 3 * phase x ∂μ‖ ≤
      B * ∫ x, ‖f x‖ ^ 2 ∂μ := by
…

theorem OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_minor_cubic_bound line 99

Source documentation

Continuous minor-frequency control for finite exponential polynomials, with exact coefficient energy and normalized Haar measure.

theorem polynomial_minor_cubic_bound (s : Finset ℤ) (w : ℤ → ℂ)
    (phase : UnitCircle → ℂ) (minor : Set UnitCircle)
    (hmeas : MeasurableSet minor) (B : ℝ) (hB : 0 ≤ B)
    (hminor : ∀ x ∈ minor, ‖polynomial s w x‖ ≤ B)
    (hphase : ∀ x ∈ minor, ‖phase x‖ ≤ 1) :
    ‖∫ x in minor, polynomial s w x ^ 3 * phase x ∂AddCircle.haarAddCircle‖ ≤
      B * ∑ n ∈ s, ‖w n‖ ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle, OAI.Problem337.ThreePrimeContinuousEnergy.polynomial

lemma OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_coe_real line 116
Source documentation
The circle polynomial evaluated on a real argument is the usual positive-sign exponential sum.
```
lemma polynomial_coe_real (s : Finset ℤ) (w : ℤ → ℂ) (x : ℝ) :
    polynomial s w (x : UnitCircle) =
      ∑ n ∈ s, w n * Complex.exp (2 * Real.pi * Complex.I * n * x) := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.polynomial, OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle
theorem OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_parseval_interval line 122
Source documentation
Parseval on the usual unit interval, with Lebesgue measure.
```
theorem polynomial_parseval_interval (s : Finset ℤ) (w : ℤ → ℂ) :
    (∫ x : ℝ in 0..1, ‖polynomial s w (x : UnitCircle)‖ ^ 2) =
      ∑ n ∈ s, ‖w n‖ ^ 2 := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.polynomial, OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle

theorem OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_interval_minor_cubic_bound line 135

Source documentation

The classical continuous minor-arc norm bound. The minor set can be any measurable subset of [0,1]; the phase is arbitrary of modulus at most one.

theorem polynomial_interval_minor_cubic_bound (s : Finset ℤ) (w : ℤ → ℂ)
    (phase : ℝ → ℂ) (minor : Set ℝ) (hmeas : MeasurableSet minor)
    (hsubset : minor ⊆ Set.Icc 0 1) (B : ℝ) (hB : 0 ≤ B)
    (hminor : ∀ x ∈ minor, ‖polynomial s w (x : UnitCircle)‖ ≤ B)
    (hphase : ∀ x ∈ minor, ‖phase x‖ ≤ 1) :
    ‖∫ x in minor, polynomial s w (x : UnitCircle) ^ 3 * phase x‖ ≤
      B * ∑ n ∈ s, ‖w n‖ ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.polynomial, OAI.Problem337.ThreePrimeContinuousEnergy.UnitCircle

def OAI.Problem337.ThreePrimeContinuousEnergy.natPolynomial line 156
Source documentation
A naturally indexed exponential sum, in the ordinary real phase variable.
```
def natPolynomial (s : Finset ℕ) (w : ℕ → ℂ) (x : ℝ) : ℂ :=
…
```
lemma OAI.Problem337.ThreePrimeContinuousEnergy.polynomial_nat_image line 159
lemma OAI.Problem337.ThreePrimeContinuousEnergy.nat_image_energy line 168
theorem OAI.Problem337.ThreePrimeContinuousEnergy.nat_polynomial_parseval_interval line 178
Source documentation
Exact unit-interval energy for arbitrary naturally indexed finite sums.
```
theorem nat_polynomial_parseval_interval (s : Finset ℕ) (w : ℕ → ℂ) :
    (∫ x : ℝ in 0..1, ‖natPolynomial s w x‖ ^ 2) = ∑ n ∈ s, ‖w n‖ ^ 2 := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.natPolynomial

theorem OAI.Problem337.ThreePrimeContinuousEnergy.nat_polynomial_interval_minor_cubic_bound line 184

Source documentation

The continuous cubic minor-arc estimate in natural-frequency notation.

theorem nat_polynomial_interval_minor_cubic_bound (s : Finset ℕ) (w : ℕ → ℂ)
    (phase : ℝ → ℂ) (minor : Set ℝ) (hmeas : MeasurableSet minor)
    (hsubset : minor ⊆ Set.Icc 0 1) (B : ℝ) (hB : 0 ≤ B)
    (hminor : ∀ x ∈ minor, ‖natPolynomial s w x‖ ≤ B)
    (hphase : ∀ x ∈ minor, ‖phase x‖ ≤ 1) :
    ‖∫ x in minor, natPolynomial s w x ^ 3 * phase x‖ ≤
      B * ∑ n ∈ s, ‖w n‖ ^ 2 := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousEnergy.natPolynomial