FourierEnergy.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The real Hilbert formulation applies to the realification of a complex L² space: real parts of complex inner products are real inner products.

lemma OAI.TriangularBilliards.Analysis.RotationalCR.projection_covariant line 35
lemma OAI.TriangularBilliards.Analysis.RotationalCR.add line 51
lemma OAI.TriangularBilliards.Analysis.RotationalCR.smul line 62
lemma OAI.TriangularBilliards.Analysis.RotationalCR.norm_eq_of_second line 81
lemma OAI.TriangularBilliards.Analysis.RotationalCR.projected_norm_eq line 102
lemma OAI.TriangularBilliards.Analysis.real_parts_CR_algebra line 113
lemma OAI.TriangularBilliards.Analysis.imag_parts_CR_algebra line 124
lemma OAI.TriangularBilliards.Analysis.CircleAction.projection_commute line 144
lemma OAI.TriangularBilliards.Analysis.CircleAction.bessel_reindex line 150

lemma OAI.TriangularBilliards.Analytic.sum_products_le line 168

Source documentation

The finite Cauchy–Schwarz bound used in the localized parity recurrence.

lemma sum_products_le {ι : Type uIota} (s : Finset ι) (a b : ι → ℝ)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
    (ha : (∑ i ∈ s, (a i) ^ 2) ≤ A ^ 2)
    (hb : (∑ i ∈ s, (b i) ^ 2) ≤ B ^ 2) :
    (∑ i ∈ s, a i * b i) ≤ A * B := by
…

lemma OAI.TriangularBilliards.Analytic.parity_energy_finite line 184

Source documentation

Exact finite telescoping plus localization. The sequences a and b are the norms of the two factors restricted to the spatial support of Xw.

lemma parity_energy_finite (D a b : ℕ → ℝ) {A B : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hrec : ∀ k, D k - D (k + 1) ≤ a k * b k)
    (ha : ∀ n, (∑ k ∈ range n, (a k) ^ 2) ≤ A ^ 2)
    (hb : ∀ n, (∑ k ∈ range n, (b k) ^ 2) ≤ B ^ 2)
    (n : ℕ) : D 0 - D n ≤ A * B := by
…

lemma OAI.TriangularBilliards.Analytic.parity_energy line 199

Source documentation

The infinite-tail passage in the energy estimate. Only the regularized test field needs its terminal energies to tend to zero; no decay is required of the invariant field.

lemma parity_energy (D a b : ℕ → ℝ) {A B : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hrec : ∀ k, D k - D (k + 1) ≤ a k * b k)
    (ha : ∀ n, (∑ k ∈ range n, (a k) ^ 2) ≤ A ^ 2)
    (hb : ∀ n, (∑ k ∈ range n, (b k) ^ 2) ≤ B ^ 2)
    (hD : Tendsto D atTop (𝓝 0)) : D 0 ≤ A * B := by
…

lemma OAI.TriangularBilliards.Analytic.inner_sum_difference line 214
Source documentation
The norm-difference identity for the Cauchy–Riemann recurrence.
```
lemma inner_sum_difference (u v : E) :
    inner ℝ (u + v) (u - v) = ‖u‖ ^ 2 - ‖v‖ ^ 2 := by
…
```

lemma OAI.TriangularBilliards.Analytic.coefficient_energy line 223

Source documentation

A version of the energy estimate with the Hilbert-space coefficient factors still visible. The equality of the two Cauchy–Riemann norms enters as hnorm; it is not asserted for nonsmooth invariant functions here.

lemma coefficient_energy (a b : ℕ → E) {A B : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hnorm : ∀ k, ‖a k‖ = ‖b k‖)
    (hX : ∀ n, (∑ k ∈ range n, ‖a k + b (k + 1)‖ ^ 2) ≤ A ^ 2)
    (hY : ∀ n, (∑ k ∈ range n, ‖a k - b (k + 1)‖ ^ 2) ≤ B ^ 2)
    (htail : Tendsto (fun n => ‖a n‖ ^ 2) atTop (𝓝 0)) :
    ‖a 0‖ ^ 2 ≤ A * B := by
…

lemma OAI.TriangularBilliards.Analysis.CircleAction.real_inner_sum_sub line 246

lemma OAI.TriangularBilliards.Analysis.CircleAction.localized_CR_energy line 258

Source documentation

The support-localized coefficient estimate. R is the spatial restriction operator; angular commutation and self-adjointness are the only properties of that operator used. Terminal-mode decay follows from Bessel and is NOT a hypothesis about an invariant field.

lemma localized_CR_energy (a b : H) (j : ℤ) (R : H →L[ℂ] H)
    (hR : ∀ θ u, R (V.act θ u) = V.act θ (R u))
    (hRs : ∀ u v, inner ℂ (R u) v = inner ℂ u (R v))
    (hX : R (a+b) = a+b)
    (hnorm : ∀ k : ℤ, ‖V.projection (k+2) a‖ = ‖V.projection k b‖) :
    ‖V.projection (j+1) a‖ ^ 2 ≤ ‖a+b‖ * ‖R (a-b)‖ := by
…