OAI/Analysis/LipschitzHilbert/Estimates/CoefficientDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient decomposes exactly into its frozen main part and the angular error whose positive majorant was proved above.

  1. theorem OAI.LipschitzHilbert.analyzingCoefficient_sub line 14
  2. theorem OAI.LipschitzHilbert.angularErrorWave_eq_sub line 29
  3. theorem OAI.LipschitzHilbert.angularCoefficient_decomposition line 37