OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingOneDimensional.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.continuous_expandingOneDimKernel line 11
2. theorem OAI.DefocusingNLS.expanding_low_integral line 21
3. theorem OAI.DefocusingNLS.expanding_high_integral line 33
4. theorem OAI.DefocusingNLS.expandingOneDimKernel_integrable_bound line 45

   Source documentation

   The inverse one-dimensional weight has an integral bounded independently of L.

   theorem expandingOneDimKernel_integrable_bound (a k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) :
       IntegrableOn (expandingOneDimKernel a k L) (Ioi 0) ∧
         (∫ x in Ioi 0, expandingOneDimKernel a k L x) ≤
           1 / (a / 6) + 1 / (k / 6 - 1) := by
   …

   Mentions: OAI.DefocusingNLS.expandingOneDimKernel

5. theorem OAI.DefocusingNLS.expandingOneDimKernel_integer_sum_bound line 89

   Source documentation

   The full integer inverse-weight sum is uniformly bounded on all expanding scales.

   theorem expandingOneDimKernel_integer_sum_bound (a k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) :
       Summable (fun n : ℤ => expandingOneDimKernel a k L n) ∧
         (∑' n : ℤ, expandingOneDimKernel a k L n) ≤
           1 + 2 * (1 / (a / 6) + 1 / (k / 6 - 1)) := by
   …

   Mentions: OAI.DefocusingNLS.expandingOneDimKernel