SourceLocalPrediction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble independently chosen source predictors on their original local windows. The resulting factor is a function of the global fine-cell index.

theorem OAI.LipschitzHilbert.FiniteLineGrid.exists_patched_source_prediction line 14

Source documentation

Probability-normalized local factors patch to a nonnegative global factor with ordinary cell averages, preserving the pointwise comparison.

theorem exists_patched_source_prediction (g : FiniteLineGrid) (coarse fine : ℕ)
    (hcf : coarse ≤ fine) (hf : fine ≤ g.depth)
    (good : Set ℝ) (beta error : ℝ → ℝ) (F : ℕ → ℝ → ℝ)
    (hF : ∀ i < g.branching^coarse, ∀ x, 0 ≤ F i x)
    (hint : ∀ i < g.branching^coarse,
      Integrable (F i) (intervalProbability (g.lineWindow coarse i (fine-coarse)).origin
        ((g.lineWindow coarse i (fine-coarse)).origin+(g.lineWindow coarse i (fine-coarse)).width)))
    (haverage : ∀ i < g.branching^coarse,
      (∫ x, F i x ∂intervalProbability (g.lineWindow coarse i (fine-coarse)).origin
        ((g.lineWindow coarse i (fine-coarse)).origin+(g.lineWindow coarse i (fine-coarse)).width)) ≤ 1)
    (hconstant : ∀ i < g.branching^coarse, ∀ x y,
      (g.lineWindow coarse i (fine-coarse)).index (fine-coarse) x =
…

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