OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingCoefficientCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact action for coefficients approximated by fixed compact profiles

  1. def OAI.DefocusingNLS.ExpandingCompactApproximation line 18

    Source documentation

    Uniform eventual approximation in the actual expanding norm by sampled compact functions.

    def ExpandingCompactApproximation (a k : ℝ) (ha1 : a < 1) (hk : 8 < k)
    (L : ℕ → ℝ) (hL : ∀ n, 1 ≤ L n) (q : ℕ → FourierL2) : Prop :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  2. theorem OAI.DefocusingNLS.tendsto_expandingApproximate_commutator line 24
  3. theorem OAI.DefocusingNLS.tendsto_expandingApproximate_lowEnergy_product line 55