SourceNormalizedDecay.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

At the source parameters, the exact mass-rescaling errors are bounded by a fixed polynomial times the inverse square root of the step.

theorem OAI.LipschitzHilbert.source_scale_exponent_bound line 13
theorem OAI.LipschitzHilbert.eventually_source_mass_rescaling_error line 22
theorem OAI.LipschitzHilbert.eventually_source_transition_error line 50

theorem OAI.LipschitzHilbert.eventually_source_relative_product line 84

Source documentation

Multiplying the parent-mass and transition factors preserves the same polynomial inverse-square-root scale.

theorem eventually_source_relative_product (B b : ℝ) (_hB : 0 ≤ B) :
    ∀ᶠ L : ℝ in atTop, ∀ q r : ℝ, 0 ≤ q → 0 ≤ r →
      q ≤ B*L^b/Real.sqrt (SourceParameters.step L) →
      r ≤ B*L^b/Real.sqrt (SourceParameters.step L) →
      q+r+q*r ≤ (3*B)*L^b/Real.sqrt (SourceParameters.step L) := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step