SourceAngularErrorTail.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The wide source cone costs only the proved logarithmic source sum. Empty scales are removed before the reference-interval moment estimate.

theorem OAI.LipschitzHilbert.LineErrorSources.restrictLength_term_eq line 17
theorem OAI.LipschitzHilbert.AngularErrorFamily.error_le_restricted_majorant line 34
Source documentation
Every actual packet is short, even if the original index horizon contains empty longer scales.
```
theorem error_le_restricted_majorant (P : AngularErrorFamily N κ ι) (H : ℝ)
    (hshort : ∀ j (_u : ι j), P.length j ≤ H) (y x : ℝ) :
    P.error y x ≤ ((P.sources y).restrictLength H).majorant x := by
…
```
Mentions: OAI.LipschitzHilbert.AngularErrorFamily

theorem OAI.LipschitzHilbert.AngularErrorFamily.eventually_source_error_budgets line 53

Source documentation

The exact dyadic source branching gives polynomial error-source budgets without any dependence on the wide carrier constant.

theorem eventually_source_error_budgets (p : ℝ) (J₀ : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : AngularErrorFamily N κ ι),
      P.sourceAmplitude ≤ L^p → P.wideExponent ≤ J₀ →
      P.exponent = SourceParameters.stepExponent L*SourceParameters.blockCount L →
      ∀ y, (P.sources y).sourceBound ≤ L^(p+3) ∧ (P.sources y).sumBound ≤ L^(p+3) := by
…

Mentions: OAI.LipschitzHilbert.AngularErrorFamily, OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount

theorem OAI.LipschitzHilbert.AngularErrorFamily.eventually_source_error_tail line 127

Source documentation

The actual angular error has a polynomial threshold and arbitrary exponential tail on every binary reference interval of retained lengths.

theorem eventually_source_error_tail (p J : ℝ) (hp : 0 ≤ p) (hJ : 0 ≤ J) (J₀ : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : AngularErrorFamily N κ ι),
      P.sourceAmplitude ≤ L^p → P.wideExponent ≤ J₀ →
      P.exponent = SourceParameters.stepExponent L*SourceParameters.blockCount L →
      ∀ (y : ℝ) (grid : FiniteLineGrid), grid.branching = 2 →
      (∀ j (_u : ι j), P.length j ≤ grid.width) →
      grid.lineMeasure {x | L^(p+7) ≤ P.error y x} ≤
        ENNReal.ofReal (Real.exp (-J*L))*grid.lineMeasure univ := by
…

Mentions: OAI.LipschitzHilbert.AngularErrorFamily, OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.FiniteLineGrid