SourceLabeledErrorTail.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The bounded active-label overlap gives the same logarithmic dyadic source budget and exponential error tail, with no total-label count.

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

theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.eventually_source_error_budgets line 41

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 : ℕ) (Λ : Fin N → Type) (κ : Type) (ι : ∀ j, Λ j → Type)
      [∀ j, Fintype (Λ j)] [Fintype κ] [∀ j b, Fintype (ι j b)] (P : LabeledAngularErrorFamily 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.LabeledAngularErrorFamily, OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount

theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.eventually_source_error_tail line 115

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 : ℕ) (Λ : Fin N → Type) (κ : Type) (ι : ∀ j, Λ j → Type)
      [∀ j, Fintype (Λ j)] [Fintype κ] [∀ j b, Fintype (ι j b)] (P : LabeledAngularErrorFamily N Λ κ ι),
      P.sourceAmplitude ≤ L^p → P.wideExponent ≤ J₀ →
      P.exponent = SourceParameters.stepExponent L*SourceParameters.blockCount L →
      ∀ (y : ℝ) (grid : FiniteLineGrid), grid.branching = 2 →
      (∀ j b (_u : ι j b), 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.LabeledAngularErrorFamily, OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.FiniteLineGrid

theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.eventually_source_error_physical_tail line 139

Source documentation

The labeled error tail on every original physical interval.

theorem eventually_source_error_physical_tail (p J : ℝ) (hp : 0 ≤ p) (hJ : 0 ≤ J)
    (J₀ : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (N : ℕ) (Λ : Fin N → Type) (κ : Type) (ι : ∀ j, Λ j → Type)
      [∀ j, Fintype (Λ j)] [Fintype κ] [∀ j b, Fintype (ι j b)]
      (P : LabeledAngularErrorFamily N Λ κ ι),
      P.sourceAmplitude ≤ L^p → P.wideExponent ≤ J₀ →
      P.exponent = SourceParameters.stepExponent L*SourceParameters.blockCount L →
      ∀ (y u H : ℝ), 0 < H → (∀ j b (_i : ι j b), P.length j ≤ H) →
      (volume.restrict (Ico u (u+H))) {x | L^(p+7) ≤ P.error y x} ≤
        ENNReal.ofReal (Real.exp (-J*L))*ENNReal.ofReal H := by
…

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