OAI/Analysis/LipschitzHilbert/Trees/SourceBalancedBlend.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The balanced source prediction after blending with one. All denominator and numerator bounds are obtained from the actual finite child data.

  1. theorem OAI.LipschitzHilbert.source_energyRatio_log_upper line 14

    Source documentation

    A denominator at least one leaves the same logarithmic numerator bound.

    theorem source_energyRatio_log_upper {E : Type*} [NormedAddCommGroup E]
    {p d K : ℝ} (hp : 1 ≤ p) (hd : 1 ≤ d) {x : E} (hx : ‖x‖ ≤ K) :
    Real.log (energyRatio p d x) ≤ p*K := by
…

    Mentions: OAI.LipschitzHilbert.energyRatio

  2. theorem OAI.LipschitzHilbert.source_balanced_prediction_blend line 30