OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationErrorMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Natural moments of the actual labeled positive error on arbitrary binary intervals. The constant depends on the source size and logarithmic source sum, never on the number of available slope labels.

  1. def OAI.LipschitzHilbert.selectorErrorMomentBase line 15
  2. theorem OAI.LipschitzHilbert.selectorErrorMomentBase_pos line 19
  3. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_joint_continuous line 29
  4. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_moment_uniform line 43

    Source documentation

    Every source family has the same polynomial moment bound on every binary interval longer than its retained scales.

    theorem error_moment_uniform (P : LabeledAngularErrorFamily N Λ κ ι)
    (B : ℝ) (_hB : 0 ≤ B)
    (hs : ∀ y, (P.sources y).sourceBound ≤ B)
    (ht : ∀ y, (P.sources y).sumBound ≤ B)
    (grid : FiniteLineGrid) (hg : grid.branching = 2)
    (hshort : ∀ j b (_u : ι j b), P.length j ≤ grid.width)
    (y : ℝ) (n : ℕ) (hn : 1 ≤ n) :
    (∫⁻ x, (ENNReal.ofReal (P.error y x))^n ∂grid.lineMeasure) ≤
      (ENNReal.ofReal (selectorErrorMomentBase B*(n:ℝ)))^n*grid.lineMeasure univ := by
…

    Mentions: OAI.LipschitzHilbert.LabeledAngularErrorFamily, OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.selectorErrorMomentBase