SourceStoppedIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local source predictors integrate on the original line grid. The stopping argument supplies the total error from the actual mass cutoff.

theorem OAI.LipschitzHilbert.source_local_path_integral line 17

Source documentation

The independently constructed local predictors suffice for the whole weighted path integral; no joint measurability of their choices is needed.

theorem source_local_path_integral
    (g : FiniteLineGrid) (T : SlopeBox) (K D y E : ℝ)
    (hK : 1 ≤ K) (hD : 0 ≤ D) (hwidth : g.width ≤ T.length)
    (level : ℕ → ℕ) (count : ℕ) (hlevel : ∀ j ≤ count, level j ≤ g.depth)
    (hmono : ∀ j < count, level j ≤ level (j+1))
    (good : Set ℝ) (beta error : ℕ → ℝ → ℝ) (F : ℕ → ℕ → ℝ → ℝ)
    (hF : ∀ j < count, ∀ i < g.branching^level j, ∀ x, 0 ≤ F j i x)
    (hint : ∀ j < count, ∀ i < g.branching^level j,
      Integrable (F j i) (intervalProbability
        (g.lineWindow (level j) i (level (j+1)-level j)).origin
        ((g.lineWindow (level j) i (level (j+1)-level j)).origin+
          (g.lineWindow (level j) i (level (j+1)-level j)).width)))
…

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

theorem OAI.LipschitzHilbert.eventually_source_stopped_path_integral line 73

Source documentation

At the source cutoff the total prediction error is at most one. Thus all the local factors give a uniform weighted line integral.

theorem eventually_source_stopped_path_integral (C A_M : ℝ)
    (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (g : FiniteLineGrid) (T : SlopeBox) (K D y N : ℝ),
      1 ≤ K → 0 ≤ D → g.width ≤ T.length → 0 < N → Real.log N ≤ 2*L →
    ∀ (level : ℕ → ℕ) (count : ℕ), (∀ j ≤ count, level j ≤ g.depth) →
      (∀ j < count, level j ≤ level (j+1)) →
    ∀ (good : Set ℝ) (beta error snapshot : ℕ → ℝ → ℝ) (n : ℝ → ℕ → ℝ)
      (stop : ℝ → ℕ) (F : ℕ → ℕ → ℝ → ℝ),
    (∀ j < count, ∀ i < g.branching^level j, ∀ x, 0 ≤ F j i x) →
    (∀ j < count, ∀ i < g.branching^level j,
      Integrable (F j i) (intervalProbability
…

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