SourceMarkedFactorsIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrate the already patched source factors. Their normalizations are exact, while the forward mass path pays the pointwise marked errors.

theorem OAI.LipschitzHilbert.source_marked_factors_integral line 14

theorem OAI.LipschitzHilbert.eventually_source_marked_drop_budget line 70

Source documentation

Actual pointwise drops can pay the doubled snapshot error.

theorem eventually_source_marked_drop_budget (C A_M : ℝ)
    (hC : 0 ≤ C) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop, ∀ (n : ℕ → ℝ) (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 ∈ Finset.range count, if marked j then
          (2*SourceParameters.step L^(-(1/32:ℝ)))*pathDrop n j else 0) ≤ 1 := by
…

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