OAI/Analysis/LipschitzHilbert/Phase/InterpolationFamily.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Analytic families for the finite Fourier interpolation

The magnitude interpolation in §7 keeps each complex phase fixed. Zero coefficients remain zero. The identities below give exact unit boundary norms for the coefficient and simple-test-function families.

  1. def OAI.LipschitzHilbert.PhaseCombinatorics.magnitudeFamily line 21
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.magnitudeFamily_zero line 25
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_magnitudeFamily_of_ne_zero line 28
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_magnitudeFamily_left line 40
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_magnitudeFamily_right line 47
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.magnitudeFamily_at_real line 54
  7. theorem OAI.LipschitzHilbert.PhaseCombinatorics.differentiable_magnitudeFamily line 64
  8. theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_magnitudeFamily_le line 77
  9. def OAI.LipschitzHilbert.PhaseCombinatorics.coefficientFamily line 99
  10. theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficientFamily_at_real line 103
  11. theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficientFamily_left_power_sum line 109
  12. theorem OAI.LipschitzHilbert.PhaseCombinatorics.coefficientFamily_right_power_sum line 119
  13. theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_magnitudeFamily_left_power_sum line 129
  14. theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_magnitudeFamily_right_power_sum line 139