OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDyadicSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A quantitative dyadic criterion for membership in the faithful Y space

Summable bounds on normalized annular pieces give convergence in Y and identify the physical representative of the sum.

  1. def OAI.DefocusingNLS.homogeneousDyadicPiece line 19
  2. theorem OAI.DefocusingNLS.homogeneousDyadicPiece_norm_le line 24
  3. theorem OAI.DefocusingNLS.summable_homogeneousDyadicPiece line 33
  4. theorem OAI.DefocusingNLS.homogeneousDyadicSeries_norm_le line 43
  5. theorem OAI.DefocusingNLS.homogeneousDyadicSeries_physical line 54
  6. theorem OAI.DefocusingNLS.exists_homogeneous_of_dyadic_representation line 73

    Source documentation

    A function reconstructed from uniformly controlled normalized annuli belongs to Y.

    theorem exists_homogeneous_of_dyadic_representation (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (v : ℕ → HomogeneousY a k) (C : ℝ) (hC : ∀ n, ‖v n‖ ≤ C)
    (Q : E → ℂ)
    (hQ : ∀ y, Q y = ∑' n, (((2 : ℝ) ^ n) ^ (-2 * a) : ℝ) *
      homogeneousPhysicalCLM a k ha ha1 hk (v n) (((2 : ℝ) ^ n)⁻¹ • y)) :
    ∃ q : HomogeneousY a k, (∀ y, homogeneousPhysicalCLM a k ha ha1 hk q y = Q y) ∧
      ‖q‖ ≤ C / (1 - 2 ^ (-a)) := by
…

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM