OAI/Analysis/LipschitzHilbert/Trees/SourceErrorTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial thresholds for the actual positive convolution error. Only the source bound and its logarithmic scale sum enter the constants.

  1. def OAI.LipschitzHilbert.LineErrorSources.momentBase line 16
  2. theorem OAI.LipschitzHilbert.LineErrorSources.momentBase_pos line 20
  3. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_moment_natural line 28
  4. theorem OAI.LipschitzHilbert.LineErrorSources.eventually_error_polynomial_tail line 49

    Source documentation

    A single order, chosen before the source family and interval, gives the desired tail. No error majorant or concentration estimate is assumed.

    theorem eventually_error_polynomial_tail (a J : ℝ) (ha : 0 ≤ a) (hJ : 0 ≤ J) :
    ∀ᶠ L : ℝ in atTop, ∀ (N : ℕ) (P : LineErrorSources N)
      (grid : FiniteLineGrid), grid.branching = 2 →
      (∀ j, grid.width < P.length j → P.source j = 0) → P.sourceBound ≤ L^a → P.sumBound ≤ L^a →
      grid.lineMeasure {x | L^(a+4) ≤ P.majorant x} ≤
        ENNReal.ofReal (Real.exp (-J*L))*grid.lineMeasure univ := by
…

    Mentions: OAI.LipschitzHilbert.LineErrorSources, OAI.LipschitzHilbert.FiniteLineGrid