OAI/Analysis/LipschitzHilbert/Phase/SourceLabeledAngularErrorData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The labeled dyadic error family formed from the original physical packets and selectors, with an exact measure-preserving coefficient identity.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.angularErrorFamily line 33
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalAngularErrorCoefficient line 83
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angularErrorFamily_coefficient line 90
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalAngularError line 112

    Source documentation

    The original positive error sum evaluated at a physical point.

    def physicalAngularError (t a : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ) (z : ℝ×ℝ) : ℝ :=
…
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angularErrorFamily_error line 119
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalAngularError_measurable line 138