SourceSnapshotChoice.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Snapshots are chosen only on one fixed line. A cell missing the good set has the constant factor one. No measurable choice across lines is used.

theorem OAI.LipschitzHilbert.FiniteLineGrid.exists_marked_prediction_from_snapshots line 15

Source documentation

Patch local predictors selected at good snapshots. Factor-two drop comparison converts their snapshot errors into actual pointwise errors.

theorem exists_marked_prediction_from_snapshots (g : FiniteLineGrid)
    (coarse fine : ℕ) (hcf : coarse ≤ fine) (hf : fine ≤ g.depth)
    (marked : ℕ → Prop) (good : Set ℝ) (beta u : ℝ → ℝ)
    (ρ : ℝ) (hρ : 0 ≤ ρ)
    (hpredict : ∀ i < g.branching^coarse, marked i →
      ∀ x₀ ∈ g.cell coarse i ∩ good,
      ∃ F : ℝ → ℝ,
        (∀ x, 0 ≤ F x) ∧
        Integrable F (intervalProbability (g.lineWindow coarse i (fine-coarse)).origin
          ((g.lineWindow coarse i (fine-coarse)).origin+(g.lineWindow coarse i (fine-coarse)).width)) ∧
        (∫ x, F x ∂intervalProbability (g.lineWindow coarse i (fine-coarse)).origin
          ((g.lineWindow coarse i (fine-coarse)).origin+(g.lineWindow coarse i (fine-coarse)).width)) ≤ 1 ∧
…

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