PredictionBlend.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the residual denominator error by the actual convex blend.

theorem OAI.LipschitzHilbert.blended_prediction_pos line 12

theorem OAI.LipschitzHilbert.blended_prediction_log_gain line 21

Source documentation

Concavity provides a gain measured by the negative logarithm of the unblended prediction.

theorem blended_prediction_log_gain {b θ : ℝ} (hb : 0 < b)
    (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) :
    -θ * Real.log b ≤ Real.log ((1 - θ) * b + θ) - Real.log b := by
…

theorem OAI.LipschitzHilbert.blended_prediction_domination line 31

Source documentation

The coefficient of the residual denominator can be canceled by choosing the blending weight at least as large as its error coefficient.

theorem blended_prediction_domination {β b θ a e r d u : ℝ}
    (hβ : 0 < β) (hb : 0 < b) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1)
    (hr : 0 ≤ r) (he : e ≤ θ)
    (hcomparison : Real.log β - Real.log b ≤ a * u + e * r)
    (hdeficit : r - d * u ≤ -Real.log b) :
    β ≤ Real.exp ((a + θ * d) * u) * ((1 - θ) * b + θ) := by
…

theorem OAI.LipschitzHilbert.balanced_blended_prediction_domination line 50

Source documentation

In the balanced case u ≥ 1/2, a bounded model logarithm has the same relative-drop form after blending.

theorem balanced_blended_prediction_domination {β b θ a d u : ℝ}
    (hβ : 0 < β) (hb : 0 < b) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1)
    (hd : 0 ≤ d) (hu : 1 / 2 ≤ u)
    (hcomparison : Real.log β - Real.log b ≤ a * u)
    (hupper : Real.log b ≤ d) :
    β ≤ Real.exp ((a + 2 * θ * d) * u) * ((1 - θ) * b + θ) := by
…