OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousWeightedObservation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Physical L² observation with an actual square-integrable coefficient

Multiplication by a fixed L² coefficient sends bounded weakly null data in the faithful homogeneous space to zero in physical L². In particular this applies to every smooth compactly supported part of a potential coefficient.

  1. theorem OAI.DefocusingNLS.homogeneousPhysical_point_bound line 19
  2. theorem OAI.DefocusingNLS.homogeneousPhysical_weighted_memLp line 29
  3. def OAI.DefocusingNLS.homogeneousWeightedObservationValue line 41
  4. theorem OAI.DefocusingNLS.homogeneousWeightedObservationValue_ae line 47
  5. theorem OAI.DefocusingNLS.homogeneousWeightedObservationValue_norm_le line 53
  6. def OAI.DefocusingNLS.homogeneousWeightedObservation line 68
  7. theorem OAI.DefocusingNLS.homogeneousWeightedObservation_norm_sq line 95
  8. theorem OAI.DefocusingNLS.tendsto_homogeneousPhysical_weighted_L2_of_weakNull line 109