DominantPredictionBlend.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Relative-drop comparison and absorption for the dominant path

The concrete path-motion bounds from §9 are substituted in the proved logarithmic comparison. The residual fraction is then absorbed by the actual convex blend, giving a multiplicative error proportional to the path drop.

theorem OAI.LipschitzHilbert.dominant_prediction_log_comparison_of_errors line 22

Source documentation

Equation (src-26) with explicit universal constants. A accounts for the absolute constants in the hierarchy motion estimates.

theorem dominant_prediction_log_comparison_of_errors
    {p C C' R R' K A ε u : ℝ} (hp : 4 ≤ p) (hA : 1 ≤ A) (hK : 1 ≤ K)
    (hε : 0 ≤ ε) (hu : 0 ≤ u) (hC0 : 0 ≤ C) (hC1 : C ≤ 1)
    (hR : 0 ≤ R) (hRR' : R ≤ R') (Y Y' Z Z' : E)
    (hY : ‖Y‖ ≤ K) (hY' : ‖Y'‖ ≤ K)
    (hCdrop : 1 - C ≤ A * u) (hZ : ‖Z‖ ≤ K * u)
    (hYmove : ‖Y' - Y‖ ≤ A * ε * K) (hCmove : |C' - C| ≤ A * ε * u)
    (hZmove : ‖Z' - Z‖ ≤ A * ε * K * u)
    (hsmall : Real.exp (A * p * ε * K) ≤ 2) :
    Real.log (energyRatio p (1 + ‖Y'‖ ^ p + R') (C' • Y' + Z')) -
      Real.log (energyRatio p (1 + ‖Y‖ ^ p + R) (C • Y + Z)) ≤
      (12 * A ^ 2 * p ^ 2 * K ^ 2 * ε) * u +
…

Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.dominant_prediction_blended_domination line 94

Source documentation

The actual dominant-path prediction is bounded by the normalized model blend, with no surviving error proportional to the residual denominator.

theorem dominant_prediction_blended_domination
    {p C C' R R' K A ε u θ : ℝ} (hp : 4 ≤ p) (hA : 1 ≤ A) (hK : 1 ≤ K)
    (hε : 0 ≤ ε) (hu : 0 ≤ u) (hC0 : 0 ≤ C) (hC1 : C ≤ 1)
    (hR : 0 ≤ R) (hRR' : R ≤ R') (Y Y' Z Z' : E)
    (hY : ‖Y‖ ≤ K) (hY' : ‖Y'‖ ≤ K)
    (hCdrop : 1 - C ≤ A * u) (hZ : ‖Z‖ ≤ K * u)
    (hYmove : ‖Y' - Y‖ ≤ A * ε * K) (hCmove : |C' - C| ≤ A * ε * u)
    (hZmove : ‖Z' - Z‖ ≤ A * ε * K * u)
    (hsmall : Real.exp (A * p * ε * K) ≤ 2)
    (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) (habsorb : 2 * A * p * ε * K ≤ θ) :
    energyRatio p (1 + ‖Y'‖ ^ p + R') (C' • Y' + Z') ≤
      Real.exp ((12 * A ^ 2 * p ^ 2 * K ^ 2 * ε + θ * (p * K)) * u) *
…

Mentions: OAI.LipschitzHilbert.energyRatio