OAI/Analysis/LipschitzHilbert/Phase/SourceAmplitudeInterpolation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original source family satisfies the analytic simplex estimate. Only its vertex moments remain as input; measurability, analytic slices, bounded exhaustion, and the full-set limiting argument are proved here.

  1. def OAI.LipschitzHilbert.AngularGrid.sourceShiftFamily line 16
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceShiftFamily_diagonal_lp line 24