SourceStoppedRecurrence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The source residual identities on the actual mass-stopped path. A unary step cannot terminate the distinguished top while its mass is active.

theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_ne_zero_eligible line 15
theorem OAI.LipschitzHilbert.AngularGrid.source_unary_next_eligible line 23
theorem OAI.LipschitzHilbert.AngularGrid.source_stopped_unary_recurrence line 35

theorem OAI.LipschitzHilbert.AngularGrid.source_stopped_residual_free_ratio line 75

Source documentation

Removing the actual block residual gives exactly the predictor used in the physical marked integral, with the original child denominator.

theorem source_stopped_residual_free_ratio {Kb : ℕ} (g : AngularGrid) (tops : Finset τ)
    (slope precision : τ → ℝ) (cutoff : ℝ) (weight : τ → X → ℝ)
    (hprecision : ∀ t ∈ tops, 0 ≤ precision t) (hweight : ∀ t x, 0 < weight t x)
    (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → τ)
    (stop : σ → ℕ) (value : X → σ → EuclideanSpace ℂ κ)
    (phase : ℕ → ℂ) (a α p μ : ℝ) (hrelation : p*μ = α-1)
    (hassigned : ∀ q ∈ packets, assigned q ∈ tops)
    (heligible : ∀ q ∈ packets, g.eligible cutoff (precision (assigned q)) (stop q))
    (hKb : 0 < Kb) (tag : Fin Kb) (top : τ) (htop : top ∈ tops) (x : X) (j : ℕ)
    (he : g.eligible cutoff (precision top) (ShiftedBlocks.endpoint tag j)) :
    let residual := g.packetResidual packets (fun q => slope (assigned q)) stop
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint