OAI/Analysis/LipschitzHilbert/Fourier/ComplexLineAverage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.lintegral_square_condExp_le line 16
2. theorem OAI.LipschitzHilbert.enorm_complex_sq line 30
3. theorem OAI.LipschitzHilbert.lintegral_complex_euclidean_sq line 39
4. def OAI.LipschitzHilbert.FiniteLineGrid.complexAverage line 59
5. theorem OAI.LipschitzHilbert.FiniteLineGrid.complexAverage_re line 64
6. theorem OAI.LipschitzHilbert.FiniteLineGrid.complexAverage_im line 69
7. theorem OAI.LipschitzHilbert.FiniteLineGrid.complexAverage_measurable line 74
8. theorem OAI.LipschitzHilbert.FiniteLineGrid.complexAverage_energy line 83
9. theorem OAI.LipschitzHilbert.lineGrid_lepingle line 100

   Source documentation

   The actual line-cell averages satisfy the published variation bound, with the norm of the original function on the right.

   theorem lineGrid_lepingle (hL : LepingleInput) :
       ∃ C : ℝ≥0, 0 < C ∧ ∀ (g : FiniteLineGrid) (κ : Type) [Fintype κ]
         (F : ℝ → EuclideanSpace ℂ κ), Measurable F →
         (∀ k, MemLp (fun x => (F x k).re) 2 g.lineMeasure) →
         (∀ k, MemLp (fun x => (F x k).im) 2 g.lineMeasure) → ∀ N : ℕ,
           (∫⁻ x, ENNReal.ofReal (finiteCubicVariation
             (fun n => g.complexAverage g.lineMeasure F n x) N) ^ (2 / 3 : ℝ) ∂g.lineMeasure) ≤
             (C : ℝ≥0∞) ^ 2 * ∫⁻ x, ‖F x‖ₑ ^ 2 ∂g.lineMeasure := by
   …

   Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.finiteCubicVariation

10. theorem OAI.LipschitzHilbert.lineGrid_variation_comparison line 125

    Source documentation

    The comparison term is the sum of squared differences between smooth partial sums and cell means.

    theorem lineGrid_variation_comparison (hL : LepingleInput) :
        ∃ C : ℝ≥0, 0 < C ∧ ∀ (g : FiniteLineGrid) (κ : Type) [Fintype κ]
          (F : ℝ → EuclideanSpace ℂ κ) (P : ℕ → ℝ → EuclideanSpace ℂ κ),
          Measurable F → (∀ n, Measurable (P n)) →
          (∀ k, MemLp (fun x => (F x k).re) 2 g.lineMeasure) →
          (∀ k, MemLp (fun x => (F x k).im) 2 g.lineMeasure) → ∀ N : ℕ,
            (∫⁻ x, ENNReal.ofReal (finiteCubicVariation (fun n => P n x) N) ^ (2 / 3 : ℝ)
              ∂g.lineMeasure) ≤
              2 * (C : ℝ≥0∞) ^ 2 * (∫⁻ x, ‖F x‖ₑ ^ 2 ∂g.lineMeasure) +
                8 * ∑ k : Fin (N + 1), ∫⁻ x,
                  ‖P k x - g.complexAverage g.lineMeasure F k x‖ₑ ^ 2 ∂g.lineMeasure := by
    …

    Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.finiteCubicVariation