SourceSnapshotWindow.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The predictor uses displacement from a chosen good snapshot. Translate its exact probability law and line-grid indices back to physical coordinates.

theorem OAI.LipschitzHilbert.intervalProbability_map_add line 15
Source documentation
Translation of the normalized interval law, with its full remainder already included in the original predictor construction.
```
theorem intervalProbability_map_add (a b t : ℝ) :
    (intervalProbability (a-t) (b-t)).map (fun x => x+t) = intervalProbability a b := by
…
```
Mentions: OAI.LipschitzHilbert.intervalProbability
def OAI.LipschitzHilbert.FiniteLineGrid.atSnapshot line 29
theorem OAI.LipschitzHilbert.FiniteLineGrid.atSnapshot_mem_root line 32
theorem OAI.LipschitzHilbert.FiniteLineGrid.atSnapshot_rawIndex line 38
theorem OAI.LipschitzHilbert.FiniteLineGrid.atSnapshot_index line 45
theorem OAI.LipschitzHilbert.FiniteLineGrid.snapshot_displacement_le_width line 50

theorem OAI.LipschitzHilbert.FiniteLineGrid.snapshot_factor_transfer line 57

Source documentation

A predictor built in displacement coordinates has exactly the same normalized average and fine-cell constancy in the physical window.

theorem snapshot_factor_transfer (g : FiniteLineGrid) (x₀ : ℝ) (level : ℕ)
    (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) :
    Measurable (fun x => P (x-x₀)) ∧
    Integrable (fun x => P (x-x₀)) (intervalProbability g.origin (g.origin+g.width)) ∧
    (∀ x, 0 ≤ P (x-x₀)) ∧
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.intervalProbability, OAI.LipschitzHilbert.FiniteLineGrid.index

theorem OAI.LipschitzHilbert.lineShift_snapshot line 90
Source documentation
Both parameterizations name the same physical point of the reference line, so packet-motion estimates apply to the chosen snapshot.
```
theorem lineShift_snapshot (s y x₀ x : ℝ) :
    SlopeBox.lineShift s (x-x₀) (x₀,y+s*x₀) = (x,y+s*x) := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox.lineShift