SourceResidualPropagation.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Exact propagation of source residual packets. The same angular transition product occurs at every shift. A packet continuing in the path child therefore acquires a coefficient depending only on its stop level; Abel summation applies to one fixed raw packet prefix.

theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_filter_split line 20

theorem OAI.LipschitzHilbert.AngularGrid.packetPathProduct_blocks line 34

Source documentation

The product of all complete block coefficients is the one common angular transition product over their union.

theorem packetPathProduct_blocks (g : AngularGrid) (transition : ℕ → ℤ → ℂ)
    (level : ℕ → ℕ) (hlevel : Monotone level) (s : ℝ) {e f : ℕ} (hef : e ≤ f) :
    unaryPropagator (fun j => g.packetPathProduct transition (level j) (level (j+1)) s) e f =
      g.packetPathProduct transition (level e) (level f) s := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.unaryPropagator

theorem OAI.LipschitzHilbert.AngularGrid.propagated_packet_coefficient line 46

Source documentation

A packet whose top lies in the path child has the same partial transition coefficient as the path itself, through its stopping level.

theorem propagated_packet_coefficient (g : AngularGrid) (transition : ℕ → ℤ → ℂ)
    (level : ℕ → ℕ) (hlevel : Monotone level) (pathSlope packetSlope : ℝ)
    {e j stop : ℕ} (hej : e ≤ j) (hstop : level j ≤ stop) (hstop' : stop ≤ level (j+1))
    (hcell : g.index (level (j+1)) packetSlope = g.index (level (j+1)) pathSlope) :
    unaryPropagator (fun b => g.packetPathProduct transition (level b) (level (b+1)) pathSlope) e j *
      g.packetPathProduct transition (level j) stop packetSlope =
        g.packetPathProduct transition (level e) stop pathSlope := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.unaryPropagator

theorem OAI.LipschitzHilbert.AngularGrid.packetAmplitude_one_child line 59

Source documentation

Generic one-child recurrence. The complementary summand is the entire amplitude of packets whose tops leave the distinguished child.

theorem packetAmplitude_one_child (g : AngularGrid) (packets : Finset σ)
    (slope : σ → ℝ) (stop : σ → ℕ) (base : σ → E) (transition : ℕ → ℤ → ℂ)
    (keep : σ → Prop) {lower upper : ℕ} (hlu : lower ≤ upper) (s : ℝ)
    (hkeep : ∀ q ∈ packets, keep q → g.index upper (slope q) = g.index upper s)
    (hlong : ∀ q ∈ packets, upper ≤ stop q →
      g.index upper (slope q) = g.index upper s → keep q) :
    g.packetAmplitude packets slope stop base transition lower (g.index lower s) =
      g.packetPathProduct transition lower upper s •
        g.packetAmplitude packets slope stop base transition upper (g.index upper s)+
      g.packetResidual (packets.filter keep) slope stop base transition lower upper (g.index lower s)+
      g.packetAmplitude (packets.filter fun q => ¬keep q) slope stop base transition lower
        (g.index lower s) := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

def OAI.LipschitzHilbert.AngularGrid.sourceContinuingPackets line 94

theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_unary_recurrence line 102

Source documentation

The recurrence uses the actual eligible-top child, not a selected packet child or a positive-amplitude child.

theorem sourcePacketAmplitude_unary_recurrence (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (K : ℕ) (gap : ℕ → ℝ)
    (packets : Finset σ) (assigned : σ → ι) (stop : σ → ℕ)
    (value : σ → E) (phase : ℕ → ℂ) (a : ℝ) (x : X)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (heligible : ∀ q ∈ packets, g.eligible cutoff (precision (assigned q)) (stop q))
    {lower upper : ℕ} (hlu : lower ≤ upper) (pathSlope : ℝ) :
    let keep := fun q => assigned q ∈ g.cellTops tops slope precision cutoff upper
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_packet_common_weight line 150

Source documentation

The actual source coefficient is the common later-starting weight whenever the packet and path share the relevant terminal cell.

theorem source_packet_common_weight (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 : ℕ → ℂ)
    (a : ℝ) (x : X) (pathTop : ι) (htop : pathTop ∈ tops) (upper : ℕ)
    (he : g.eligible cutoff (precision pathTop) upper)
    (packetTop : ι) {start stop : ℕ} (hstop : stop ≤ upper)
    (hcell : g.index upper (slope packetTop) = g.index upper (slope pathTop)) :
    let n := fun j => g.mass tops slope precision cutoff weight j (g.index j (slope pathTop)) x
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.weighted_packet_sum_by_stop line 183

Source documentation

Grouping a finite packet sum by its actual integer stopping level.

theorem weighted_packet_sum_by_stop {σ E : Type*} [AddCommMonoid E] [Module ℂ E]
    (packets : Finset σ) (stop : σ → ℕ) (value : σ → E) (weight : ℕ → ℂ)
    (lower upper : ℕ) :
    (∑ q ∈ packets.filter (fun q => lower ≤ stop q ∧ stop q < upper),
      weight (stop q) • value q) =
    ∑ k ∈ Finset.Ico lower upper,
      weight k • ∑ q ∈ packets.filter (fun q => stop q = k), value q := by
…

theorem OAI.LipschitzHilbert.sum_consecutive_block_intervals line 214

Source documentation

Consecutive block intervals exactly fill the corresponding angular interval, regardless of their unequal lengths.

theorem sum_consecutive_block_intervals {E : Type*} [AddCommMonoid E]
    (level : ℕ → ℕ) (hlevel : Monotone level) (f : ℕ → E)
    {e b : ℕ} (heb : e ≤ b) :
    (∑ j ∈ Finset.Ico e b, ∑ k ∈ Finset.Ico (level j) (level (j+1)), f k) =
      ∑ k ∈ Finset.Ico (level e) (level b), f k := by
…

theorem OAI.LipschitzHilbert.AngularGrid.block_of_stop_unique line 229

Source documentation

Stop intervals belonging to different blocks are disjoint.

theorem block_of_stop_unique (level : ℕ → ℕ) (hlevel : StrictMono level)
    {i j k : ℕ} (hi : level i ≤ k ∧ k < level (i+1))
    (hj : level j ≤ k ∧ k < level (j+1)) : i = j := by
…

def OAI.LipschitzHilbert.AngularGrid.fixedPathResidualPackets line 241
Source documentation
The residual subset is fixed by the path and stopping levels. It does not depend on the point at which the amplitude is evaluated.
```
def fixedPathResidualPackets (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (packets : Finset σ)
    (assigned : σ → ι) (stop : σ → ℕ) (level : ℕ → ℕ) (count : ℕ) (pathSlope : ℝ) : Finset σ :=
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid
theorem OAI.LipschitzHilbert.AngularGrid.fixedPathResidualPackets_block line 248

theorem OAI.LipschitzHilbert.AngularGrid.packetResidual_continuing_eq line 268

Source documentation

Once a packet's top continues in the path child, its parent-cell condition in the residual is automatic by angular-grid nesting.

theorem packetResidual_continuing_eq (g : AngularGrid) (packets : Finset σ)
    (slope : σ → ℝ) (stop : σ → ℕ) (base : σ → E) (transition : ℕ → ℤ → ℂ)
    (keep : σ → Prop) {lower upper : ℕ} (hlu : lower ≤ upper) (s : ℝ)
    (hkeep : ∀ q ∈ packets, keep q → g.index upper (slope q) = g.index upper s) :
    g.packetResidual (packets.filter keep) slope stop base transition lower upper (g.index lower s) =
      ∑ q ∈ (packets.filter keep).filter (fun q => lower ≤ stop q ∧ stop q < upper),
        g.packetPathProduct transition lower (stop q) (slope q) • base q := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_propagated_residual_eq line 289

Source documentation

After propagation from an earlier block, the continuing residual uses the same coefficient at each stop level. Every packet remains in the deterministic path residual subset defined above.

theorem source_propagated_residual_eq (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 : ℕ → ℝ) (packets : Finset σ)
    (assigned : σ → ι) (stop : σ → ℕ) (value : σ → E) (phase : ℕ → ℂ)
    (a : ℝ) (x : X) (level : ℕ → ℕ) (hlevel : StrictMono level) (count : ℕ)
    (pathTop : ι) (htop : pathTop ∈ tops)
    {e j : ℕ} (hej : e ≤ j) (hj : j < count)
    (he : g.eligible cutoff (precision pathTop) (level (j+1))) :
    let transition := g.sourceTransition tops slope precision cutoff weight K gap phase x
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_propagated_residual_interval line 353

Source documentation

The sum of propagated residuals over consecutive blocks is one weighted stop-level interval of the fixed raw residual family.

theorem source_propagated_residual_interval (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 : ℕ → ℝ) (packets : Finset σ)
    (assigned : σ → ι) (stop : σ → ℕ) (value : σ → E) (phase : ℕ → ℂ)
    (a : ℝ) (x : X) (level : ℕ → ℕ) (hlevel : StrictMono level) (count : ℕ)
    (pathTop : ι) (htop : pathTop ∈ tops)
    {e f : ℕ} (hef : e ≤ f) (hfc : f ≤ count)
    (he : g.eligible cutoff (precision pathTop) (level f)) :
    let transition := g.sourceTransition tops slope precision cutoff weight K gap phase x
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_propagated_residual_bound line 409

Source documentation

Abel summation of the actual propagated residuals. All raw sums use the one fixed residual packet subset. The coefficient cost involves the full-root mass ratio, even for a segment starting much later.

theorem source_propagated_residual_bound (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 : ℕ → ℝ) (packets : Finset σ)
    (assigned : σ → ι) (stop : σ → ℕ) (value : σ → E) (phase : ℕ → ℂ)
    (a : ℝ) (x : X) (level : ℕ → ℕ) (hlevel : StrictMono level) (count : ℕ)
    (pathTop : ι) (htop : pathTop ∈ tops)
    {e f : ℕ} (hef : e < f) (hfc : f ≤ count)
    (he : g.eligible cutoff (precision pathTop) (level f)) (H : ℕ) (hH : level f ≤ H)
    {lower Z : ℝ} (ha : 0 ≤ a) (hlower : 0 < lower) (hZ : 0 ≤ Z)
    (hnlower : lower ≤ g.mass tops slope precision cutoff weight (level f)
      (g.index (level f) (slope pathTop)) x)
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_offchild_top_fibers line 467

Source documentation

Whole amplitudes of the tops leaving the path child. Packet coefficients still use the original full family of angular masses.

theorem source_offchild_top_fibers (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (K : ℕ) (gap : ℕ → ℝ)
    (bands : Finset σ) (stop : ι → σ → ℕ) (value : ι → σ → E)
    (he : ∀ t ∈ tops, ∀ k ∈ bands, g.eligible cutoff (precision t) (stop t k))
    (phase : ℕ → ℂ) (a : ℝ) (x : X) (lower upper : ℕ) (pathSlope : ℝ) :
    let child := g.cellTops tops slope precision cutoff upper (g.index upper pathSlope)
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.source_offchild_amplitude_bound line 504

Source documentation

The discarded-top contribution is paid by its total removed mass, not by the number of removed tops.

theorem source_offchild_amplitude_bound (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (K : ℕ) (gap : ℕ → ℝ) (bands : Finset σ) (stop : ι → σ → ℕ) (value : ι → σ → E)
    (he : ∀ t ∈ tops, ∀ k ∈ bands, g.eligible cutoff (precision t) (stop t k))
    (phase : ℕ → ℂ) (a : ℝ) (x : X) {lower upper : ℕ} (hlu : lower ≤ upper)
    (pathSlope ε : ℝ)
    (hsmall : ∀ t ∈ g.cellTops tops slope precision cutoff lower (g.index lower pathSlope),
      t ∉ g.cellTops tops slope precision cutoff upper (g.index upper pathSlope) →
      ‖g.sourcePacketAmplitude tops slope precision cutoff weight K gap bands
        (fun _ => t) (stop t) (value t) phase a x lower (g.index lower (slope t))‖ ≤ ε*weight t x) :
    let child := g.cellTops tops slope precision cutoff upper (g.index upper pathSlope)
…

Mentions: OAI.LipschitzHilbert.AngularGrid