SourceSelectorConcentrationSplit.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact original-selector interval splitting for top concentration. All three raw covariant jets use the original analyzing coefficients. Only the frozen-centered synthesis needs a variation estimate; the remaining interval is controlled by the positive angular error.

theorem OAI.LipschitzHilbert.norm_increment_le_cubicVariation line 17
theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawBand_eq_packet_sum line 39
def OAI.LipschitzHilbert.SourceLabeledLattice.selectorCenteredRawVariation line 48
Source documentation
The fixed main coefficient is the only part requiring cancellation.
```
def selectorCenteredRawVariation (i : Fin 3) (x y : ℝ) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_rawBand_split line 52
theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_rawInterval_split line 69

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_error_rawInterval_norm line 88

Source documentation

Positive angular error controls an arbitrary original interval, without a factor for its number of scales or labels.

theorem selector_error_rawInterval_norm (horder : 6 ≤ P.order)
    (i : Fin 3) (lower upper : ℕ) (hlu : lower ≤ upper) (x y : ℝ) :
    ‖(P.withProfile alt hAlt).rawInterval (P.physicalAngularErrorCoefficient t a b v g)
        i lower upper x y‖ ≤
      P.absoluteConstant*P.physicalAngularError t a b v g (x,y+t*x) := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_rawInterval_norm_le_variation_add_error line 124

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_rawInterval_joint_norm line 143

Source documentation

The raw first jet is exactly the scaled vertical covariant derivative, so the same split supplies both terms of top concentration.

theorem selector_rawInterval_joint_norm (horder : 6 ≤ P.order)
    (hb : ∀ j l k, Measurable (b j l k))
    (hb1 : ∀ j l k s, ‖b j l k s‖ ≤ 1)
    (hv : Measurable v) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
    (lower upper : ℕ) (hlu : lower ≤ upper) (hu : upper ≤ N)
    (W : ℝ) (hW : W ≤ |P.scale|) (x y : ℝ) :
    let F := fun x y => (P.withProfile alt hAlt).rawInterval
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval

theorem OAI.LipschitzHilbert.SourceLabeledLattice.selector_error_vertical_neighborhood line 179
Source documentation
The positive error majorant controls a full packet-width vertical neighborhood at a fixed cost, without a supremum over coefficients.
```
theorem selector_error_vertical_neighborhood (x y shift : ℝ) (hshift : |shift| ≤ P.width) :
    P.physicalAngularError t a b v g (x,y+shift+t*x) ≤
      (3:ℝ)^6*P.physicalAngularError t a b v g (x,y+t*x) := by
…
```