OAI/Analysis/LipschitzHilbert/Phase/SimplexTubeInterpolation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded analytic tubes preserve a common bound under finite convex combinations of their real parameters. This is the scalar interpolation step used for the finitely many shift parameters in manuscript §11.

  1. def OAI.LipschitzHilbert.phaseTubePoint line 16
  2. def OAI.LipschitzHilbert.phaseTubeLine line 19
  3. def OAI.LipschitzHilbert.phaseTubeBound line 22
  4. theorem OAI.LipschitzHilbert.phaseTubeLine_re_im line 25
  5. theorem OAI.LipschitzHilbert.convex_phaseTubeBound line 34
  6. theorem OAI.LipschitzHilbert.phaseTubeBound_finite_convex_combination line 74