OAI/Analysis/LipschitzHilbert/Trees/SourceMarkingParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual relative mass-motion error is small even after multiplication by the polynomial stopping threshold. These fixed-parameter bounds supply the source's exceptional-cell argument.

  1. theorem OAI.LipschitzHilbert.eventually_source_marking_parameters line 14
  2. theorem OAI.LipschitzHilbert.eventually_source_marking_parameters_uniform line 54

    Source documentation

    The conclusion is uniform over the source weight scale Kw≥1.

    theorem eventually_source_marking_parameters_uniform (D A_M : ℝ)
    (hD : 0 ≤ D) (hAM : 0 ≤ A_M) :
    ∀ᶠ L : ℝ in atTop, ∀ Kw : ℝ, 1 ≤ Kw →
      let δ := (5*D/Kw)/Real.sqrt (SourceParameters.step L)
…

    Mentions: OAI.LipschitzHilbert.SourceParameters.step