SourceReverseSnapshot.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The local grid used by physical packet prediction is exactly a translated window of the single reverse angular grid. No replacement partition or rounding of a block length is required.

theorem OAI.LipschitzHilbert.FiniteLineGrid.eq_of_fields line 16

theorem OAI.LipschitzHilbert.FiniteLineGrid.snapshot_prediction_transfer line 25

Source documentation

A displacement-coordinate predictor gives the same bound on the physical reference line and keeps its exact probability average.

theorem snapshot_prediction_transfer (g : FiniteLineGrid) (x₀ y s ε : ℝ)
    (level : ℕ) (beta : ℝ × ℝ → ℝ) (P : ℝ → ℝ)
    (hP : Measurable P)
    (hint : Integrable P (intervalProbability (g.atSnapshot x₀).origin
      ((g.atSnapshot x₀).origin+(g.atSnapshot x₀).width)))
    (hpos : ∀ b, 0 ≤ P b)
    (havg : (∫ b, P b ∂intervalProbability (g.atSnapshot x₀).origin
      ((g.atSnapshot x₀).origin+(g.atSnapshot x₀).width)) ≤ 1)
    (hconst : ∀ b c, (g.atSnapshot x₀).index level b =
      (g.atSnapshot x₀).index level c → P b = P c)
    (hcompare : ∀ b ∈ (g.atSnapshot x₀).root,
      beta (SlopeBox.lineShift s b (x₀,y+s*x₀)) ≤ Real.exp ε*P b) :
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.intervalProbability, OAI.LipschitzHilbert.FiniteLineGrid.index, OAI.LipschitzHilbert.FiniteLineGrid.root, OAI.LipschitzHilbert.SlopeBox.lineShift

theorem OAI.LipschitzHilbert.source_reverse_snapshot_window line 53
Source documentation
The physical block predictor uses this very translated reverse-grid window, including the shorter initial angular block.
```
theorem source_reverse_snapshot_window {K : ℕ} (g : AngularGrid) (L origin : ℝ)
    {w : ℝ} (hw : 0 < w) (σ : Fin K) (hK : 0 < K) {count j : ℕ}
    (hj : j < count) (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (i : ℕ) (x₀ : ℝ) :
    let grid := sourceReverseLineGrid g L origin hw σ count
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.sourceReverseLineGrid