OAI/Analysis/LipschitzHilbert/Estimates/ErrorSynthesisVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual error synthesis variation is bounded by its positive coefficient envelope, then by the constructed error moments.

  1. theorem OAI.LipschitzHilbert.norm_diagonalSynthesis_le line 15
  2. def OAI.LipschitzHilbert.AngularErrorFamily.synthesisVariation line 34
  3. theorem OAI.LipschitzHilbert.AngularErrorFamily.synthesisVariation_le line 38
  4. theorem OAI.LipschitzHilbert.AngularErrorFamily.synthesisVariation_moment line 50