OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationErrorSynthesis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original angular-error coefficients may synthesize a different profile. Polynomially weighting the two raw covariant jets leaves their sixth-order positive envelope, so the preceding moment theorem applies.

  1. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_interval_norm_le line 20
  2. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_synthesis_global_neighborhood line 72