OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeOperator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded whole-space free operators on the exact completion

The Fourier-side Schwartz action extends through a dense map to Y. The bound for nonnegative time is exactly exp(-a s/2).

  1. def OAI.DefocusingNLS.homogeneousFrequencyEmbedding line 18
  2. theorem OAI.DefocusingNLS.homogeneousFrequencyEmbedding_dense line 23
  3. theorem OAI.DefocusingNLS.homogeneousFrequencyEmbedding_norm_sq line 31
  4. theorem OAI.DefocusingNLS.homogeneousFrequencyEmbedding_norm_sq_integral line 43
  5. def OAI.DefocusingNLS.homogeneousFreeBound line 56
  6. theorem OAI.DefocusingNLS.exp_half_sq line 59
  7. theorem OAI.DefocusingNLS.homogeneousFreeFourier_norm_bound line 64
  8. def OAI.DefocusingNLS.homogeneousFreeOperator line 98
  9. theorem OAI.DefocusingNLS.homogeneousFreeOperator_on_Schwartz line 104
  10. theorem OAI.DefocusingNLS.homogeneousFreeOperator_norm_le line 112
  11. theorem OAI.DefocusingNLS.homogeneousFreeOperator_forward_bound line 119

    Source documentation

    The exact forward decay in the manuscript's homogeneous norm.

    theorem homogeneousFreeOperator_forward_bound (a b k s : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hs : 0 ≤ s) (f : HomogeneousY a k) :
    ‖homogeneousFreeOperator a b k s ha ha1 hk f‖ ≤ Real.exp (-a * s / 2) * ‖f‖ := by
…

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousFreeOperator