LocalSkippedPrediction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Patch local source predictions by the actual global fine-cell profile. Points outside the root share the first fiber's value, so global constancy is preserved without any extra measurable-choice requirement.

theorem OAI.LipschitzHilbert.FiniteLineGrid.nonnegative_profile_on line 14

theorem OAI.LipschitzHilbert.FiniteLineGrid.exists_patched_window_factor line 34

Source documentation

Local window factors assemble into one globally fine-cell-constant nonnegative function, with the correct average on every coarse cell.

theorem exists_patched_window_factor (g : FiniteLineGrid) (coarse fine : ℕ)
    (hcf : coarse ≤ fine) (hf : fine ≤ g.depth)
    (F : ℕ → ℝ → ℝ)
    (hF : ∀ i < g.branching^coarse, ∀ x ∈ g.cell coarse i, 0 ≤ F i x)
    (hconstant : ∀ i < g.branching^coarse, ∀ x ∈ g.cell coarse i,
      ∀ y ∈ g.cell coarse i, g.index fine x = g.index fine y → F i x = F i y)
    (haverage : ∀ i < g.branching^coarse,
      (∫ x in g.cell coarse i, F i x) ≤ volume.real (g.cell coarse i)) :
    ∃ Γ : ℝ → ℝ, Measurable Γ ∧ (∀ x, 0 ≤ Γ x) ∧
      (∀ x y, g.index fine x = g.index fine y → Γ x = Γ y) ∧
      (∀ x ∈ g.root, Γ x = F (g.index coarse x).val x) ∧
      (∀ i : Fin (g.branching^g.depth),
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid