SourceMarkedPrediction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Marking belongs to an entire coarse line cell. On every unmarked cell the prediction factor is exactly one. In particular a cell containing an inactive point cannot contribute a marked factor.

def OAI.LipschitzHilbert.FiniteLineGrid.markedValue line 18
def OAI.LipschitzHilbert.FiniteLineGrid.markedError line 22
theorem OAI.LipschitzHilbert.FiniteLineGrid.measurableSet_marked line 26
theorem OAI.LipschitzHilbert.FiniteLineGrid.measurable_markedValue line 34
theorem OAI.LipschitzHilbert.FiniteLineGrid.measurable_markedError line 38

theorem OAI.LipschitzHilbert.FiniteLineGrid.exists_marked_source_prediction line 44

Source documentation

Only marked cells require an analytic predictor. The other cells have factor one, retaining exact normalization and fine-cell constancy.

theorem exists_marked_source_prediction (g : FiniteLineGrid) (coarse fine : ℕ)
    (hcf : coarse ≤ fine) (hf : fine ≤ g.depth)
    (marked : ℕ → Prop) (good : Set ℝ) (beta error : ℝ → ℝ) (F : ℕ → ℝ → ℝ)
    (hF : ∀ i < g.branching^coarse, marked i → ∀ x, 0 ≤ F i x)
    (hint : ∀ i < g.branching^coarse, marked i →
      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, marked i →
      (∫ 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, marked i → ∀ x z,
      (g.lineWindow coarse i (fine-coarse)).index (fine-coarse) x =
…

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

theorem OAI.LipschitzHilbert.FiniteLineGrid.unmarked_of_mass_le line 108

Source documentation

The source's cellwise condition rules out marked factors as soon as the actual point has crossed its mass cutoff.

theorem unmarked_of_mass_le (g : FiniteLineGrid) (coarse : ℕ) (marked : ℕ → Prop)
    (n : ℝ → ℝ) (M : ℝ)
    (hmark : ∀ i < g.branching^coarse, marked i → ∀ x ∈ g.cell coarse i, M < n x)
    (hcoarse : coarse ≤ g.depth) {x : ℝ} (hx : x ∈ g.root) (hn : n x ≤ M) :
    ¬marked (g.index coarse x).val := by
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid

theorem OAI.LipschitzHilbert.eventually_source_marked_error line 127

Source documentation

Marked errors are a subfamily of the active forward mass-path errors. No claim that pointwise stopping is itself a coarse-cell condition is used.

theorem eventually_source_marked_error (C A_M : ℝ) (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop, ∀ (n e snapshot : ℕ → ℝ) (count : ℕ) (marked : ℕ → Prop),
    ∀ N : ℝ, 0 < N → Real.log N ≤ 2*L → n 0 ≤ L^C*N^2 →
      (∀ j, 0 ≤ n j) → Antitone n → n count ≤ L^A_M →
      (∀ j < count, marked j → L^A_M < n j) →
      (∀ j < count, marked j → snapshot j/2 ≤ pathDrop n j) →
      (∀ j < count, marked j → e j ≤ SourceParameters.step L^(-(1/32:ℝ))*snapshot j) →
      (∑ j ∈ Finset.range count, if marked j then e j else 0) ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.pathDrop, OAI.LipschitzHilbert.SourceParameters.step