OAI/Analysis/LipschitzHilbert/Estimates/AmplitudeApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite amplitude approximations converge in squared L2 energy. The cutoff is the actual disjoint union of its amplitude levels.

  1. theorem OAI.LipschitzHilbert.amplitude_scaled_piece line 18
  2. theorem OAI.LipschitzHilbert.amplitudeApprox_eq_indicator line 25
  3. theorem OAI.LipschitzHilbert.amplitudeApprox_measurable line 32
  4. theorem OAI.LipschitzHilbert.amplitudeApprox_memLp line 37
  5. theorem OAI.LipschitzHilbert.amplitudeApprox_sub_norm_le line 43
  6. theorem OAI.LipschitzHilbert.amplitudeApprox_eventually_eq line 51
  7. theorem OAI.LipschitzHilbert.amplitudeApprox_energy_tendsto line 67
  8. theorem OAI.LipschitzHilbert.amplitudeApprox_Lp_tendsto line 85