OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingWeightProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.expandingOneDimWeight_coordinate_le line 12
2. theorem OAI.DefocusingNLS.expandingWeight_product_le line 30
3. theorem OAI.DefocusingNLS.expandingSobolevWeight_inv_le_product line 86

   Source documentation

   The inverse radial weight is dominated by a product with a uniform integer sum.

   theorem expandingSobolevWeight_inv_le_product (a k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (n : frequencyLattice) :
       (expandingSobolevWeightSq a k L n)⁻¹ ≤
         2 ^ 12 * ∏ j : Fin 12, expandingOneDimKernel a k L (frequencyCoordinates n j) := by
   …

   Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeightSq, OAI.DefocusingNLS.expandingOneDimKernel, OAI.DefocusingNLS.frequencyCoordinates

4. theorem OAI.DefocusingNLS.frequencyCoordinates_injective line 98
5. theorem OAI.DefocusingNLS.sum_expandingKernel_product_le line 107

   Source documentation

   Summing the separable majorant uses only finite products and the one-dimensional sum.

   theorem sum_expandingKernel_product_le (a k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (S : Finset frequencyLattice) :
       (∑ n ∈ S, ∏ j : Fin 12, expandingOneDimKernel a k L (frequencyCoordinates n j)) ≤
         (1 + 2 * (1 / (a / 6) + 1 / (k / 6 - 1))) ^ 12 := by
   …

   Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingOneDimKernel, OAI.DefocusingNLS.frequencyCoordinates

6. theorem OAI.DefocusingNLS.summable_expandingSobolevWeight_inv line 141

   Source documentation

   The exact normalized inverse weights have a scale-independent summability bound.

   theorem summable_expandingSobolevWeight_inv (a k L : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) :
       Summable (fun n : frequencyLattice => (expandingSobolevWeightSq a k L n)⁻¹) ∧
         (∑' n : frequencyLattice, (expandingSobolevWeightSq a k L n)⁻¹) ≤
           2 ^ 12 * (1 + 2 * (1 / (a / 6) + 1 / (k / 6 - 1))) ^ 12 := by
   …

   Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingSobolevWeightSq