SourceMarkedIntegral.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Marked predictors are patched cellwise, then integrated in reverse geometric order. Their logarithmic errors are summed in the original forward angular order and paid by the actual first mass crossing.

def OAI.LipschitzHilbert.reverseMarkedValue line 16
def OAI.LipschitzHilbert.reverseMarkedError line 20

theorem OAI.LipschitzHilbert.source_marked_path_integral line 26

Source documentation

The geometric hypotheses concern increasing line levels. The local predictors, original factors, and error budget remain in forward path order.

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

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

theorem OAI.LipschitzHilbert.eventually_source_marked_path_integral line 125

Source documentation

The actual first mass crossing pays the error of every marked factor. The product is still written in forward angular order.

theorem eventually_source_marked_path_integral (C A_M : ℝ)
    (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (g : FiniteLineGrid) (T : SlopeBox) (K D y N : ℝ)
    (_hK : 1 ≤ K) (_hD : 0 ≤ D) (_hwidth : g.width ≤ T.length)
    (_hN : 0 < N) (_hlog : Real.log N ≤ 2*L)
    (level : ℕ → ℕ) (count : ℕ) (_hlevel : ∀ k ≤ count, level k ≤ g.depth)
    (_hmono : ∀ k < count, level k ≤ level (k+1))
    (good : Set ℝ) (marked : ℕ → ℕ → Prop) (beta error : ℕ → ℝ → ℝ)
    (F : ℕ → ℕ → ℝ → ℝ)
    (_hF : ∀ j < count, ∀ i < g.branching^level (ShiftedBlocks.reverseIndex count j),
      marked j i → ∀ x, 0 ≤ F j i x)
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.ShiftedBlocks.reverseIndex