SourceResidualSquare.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual residual coefficient is bounded by its assigned top's mask times a negative power of that top's weight. Grouping the resulting absolute packet envelopes by the disjoint source length bands gives the marked residual square estimate without any angular-depth factor.

theorem OAI.LipschitzHilbert.packet_length_group_norm_bound line 15
theorem OAI.LipschitzHilbert.AngularGrid.source_packet_residual_coefficient_bound line 36

theorem OAI.LipschitzHilbert.AngularGrid.source_packet_residual_norm_bound line 77

Source documentation

Exact assigned-top coefficients and a per-length absolute envelope control the complete residual of an actual source node.

theorem source_packet_residual_norm_bound {N : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (hz : ∀ k, 0 ≤ (phase k).re) (a : ℝ) (ha : 0 ≤ a) (x : X)
    (packets : Finset σ) (assigned : σ → ι) (lengthIndex : σ → Fin N)
    (stop : Fin N → ℕ) (mask : ι → ℂ) (value : σ → E)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (he : ∀ q ∈ packets, g.eligible cutoff (precision (assigned q)) (stop (lengthIndex q)))
    (C : ℝ) (hC : 0 ≤ C) (hmask : ∀ t ∈ tops, weight t x^(-a)*‖mask t‖ ≤ C)
    (lower upper : ℕ) (pathSlope : ℝ) (envelope : Fin N → ℝ)
    (henvelope : ∀ k ∈ residualLengthSet stop lower upper,
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.residualLengthSet

theorem OAI.LipschitzHilbert.AngularGrid.source_packet_residual_square_sum line 117

Source documentation

The block square estimate now has the actual source residuals on the left. All overlap and length-cardinality costs are proved above; the remaining inputs are the positive per-length reference envelopes.

theorem source_packet_residual_square_sum {N : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
    (hz : ∀ k, 0 ≤ (phase k).re) (a : ℝ) (ha : 0 ≤ a) (x : X)
    (packets : Finset σ) (assigned : σ → ι) (lengthIndex : σ → Fin N)
    (stop : Fin N → ℕ) (mask : ι → ℂ) (value : σ → E)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (he : ∀ q ∈ packets, g.eligible cutoff (precision (assigned q)) (stop (lengthIndex q)))
    (C : ℝ) (hC : 0 ≤ C) (hmask : ∀ t ∈ tops, weight t x^(-a)*‖mask t‖ ≤ C)
    (level : ℕ → ℕ) (hlevel : StrictMono level) (count : ℕ) (pathSlope : ℝ)
    (error main : Fin N → ℝ) (herror : ∀ k, 0 ≤ error k) (hmain : ∀ k, 0 ≤ main k)
…

Mentions: OAI.LipschitzHilbert.AngularGrid