DominantPathComparison.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Dominant-path logarithmic comparison

The numerator and path denominator are compared together, as in §9, pred:path-errors and equation (src-26). The derivative cancellation is proved from the actual logarithmic-energy derivative; the residual child denominator is retained with its exact fractional weight.

def OAI.LipschitzHilbert.residualLogCorrection line 22
Source documentation
The logarithmic correction from the off-path denominator.
```
def residualLogCorrection (R a : ℝ) : ℝ := a - Real.log (Real.exp a + R)
```
theorem OAI.LipschitzHilbert.hasDerivAt_residualLogCorrection line 24
theorem OAI.LipschitzHilbert.residualLogCorrection_lipschitz line 35
Source documentation
Throughout a logarithmic-energy interval of radius d, the derivative of the residual correction is at most exp d times its initial fraction.
```
theorem residualLogCorrection_lipschitz {R a b d : ℝ} (hR : 0 ≤ R)
    (hd : 0 ≤ d) (hab : |b - a| ≤ d) :
    |residualLogCorrection R b - residualLogCorrection R a| ≤
      (Real.exp d * R / (Real.exp a + R)) * |b - a| := by
…
```
Mentions: OAI.LipschitzHilbert.residualLogCorrection
theorem OAI.LipschitzHilbert.residualLogCorrection_le line 60
def OAI.LipschitzHilbert.residualFraction line 78
Source documentation
The off-path fraction of the complete child denominator.
```
def residualFraction (p R : ℝ) (Y : E) : ℝ := R / (1 + ‖Y‖ ^ p + R)
```
theorem OAI.LipschitzHilbert.residualFraction_nonneg line 80
theorem OAI.LipschitzHilbert.residual_log_energy_change line 85
def OAI.LipschitzHilbert.pathCancelledLogEnergy line 109
theorem OAI.LipschitzHilbert.log_path_ratio_eq line 113
Source documentation
Exact separation of the path denominator and the residual child mass.
```
theorem log_path_ratio_eq {p C R : ℝ} (hR : 0 ≤ R) (Y Z : E) :
    Real.log (energyRatio p (1 + ‖Y‖ ^ p + R) (C • Y + Z)) =
      pathCancelledLogEnergy p C Z Y + residualLogCorrection R (logEnergy p Y) := by
…
```
Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.pathCancelledLogEnergy, OAI.LipschitzHilbert.residualLogCorrection, OAI.LipschitzHilbert.logEnergy
theorem OAI.LipschitzHilbert.dominant_model_deficit line 123
Source documentation
The model deficit controls the residual fraction, up to the off-path numerator amplitude, exactly as in the second line of (src-26).
```
theorem dominant_model_deficit {p C R : ℝ} (hp : 1 ≤ p) (hR : 0 ≤ R)
    (hC0 : 0 ≤ C) (hC1 : C ≤ 1) (Y Z : E) :
    residualFraction p R Y - p * ‖Z‖ ≤
      -Real.log (energyRatio p (1 + ‖Y‖ ^ p + R) (C • Y + Z)) := by
…
```
Mentions: OAI.LipschitzHilbert.residualFraction, OAI.LipschitzHilbert.energyRatio
theorem OAI.LipschitzHilbert.hasFDerivAt_pathCancelledLogEnergy line 144
theorem OAI.LipschitzHilbert.norm_pathCancelledLogEnergy_derivative_le line 154

theorem OAI.LipschitzHilbert.pathCancelledLogEnergy_lipschitz line 193

Source documentation

The path numerator and path denominator change together. The resulting motion is proportional to 1-C and the off-path amplitude.

theorem pathCancelledLogEnergy_lipschitz {p C K : ℝ} (hp : 4 ≤ p)
    (hC0 : 0 ≤ C) (hC1 : C ≤ 1) (Z Y Y' : E) (hY : ‖Y‖ ≤ K) (hY' : ‖Y'‖ ≤ K) :
    |pathCancelledLogEnergy p C Z Y' - pathCancelledLogEnergy p C Z Y| ≤
      (p * (1 - C) + 4 * p ^ 2 * ((1 - C) * K + ‖Z‖)) * ‖Y' - Y‖ := by
…

Mentions: OAI.LipschitzHilbert.pathCancelledLogEnergy

theorem OAI.LipschitzHilbert.dominant_prediction_log_comparison line 210

Source documentation

The first line of (src-26), before inserting the hierarchy's motion constants. The numerator, path cancellation, and residual fraction have separate exact coefficients. Increasing the actual residual only helps.

theorem dominant_prediction_log_comparison {p C C' R R' K : ℝ}
    (hp : 4 ≤ p) (hC0 : 0 ≤ C) (hC1 : C ≤ 1) (hR : 0 ≤ R) (hRR' : R ≤ R')
    (Y Y' Z Z' : E) (hY : ‖Y‖ ≤ K) (hY' : ‖Y'‖ ≤ K) :
    Real.log (energyRatio p (1 + ‖Y'‖ ^ p + R') (C' • Y' + Z')) -
      Real.log (energyRatio p (1 + ‖Y‖ ^ p + R) (C • Y + Z)) ≤
      p * (|C' - C| * ‖Y'‖ + ‖Z' - Z‖) +
        (p * (1 - C) + 4 * p ^ 2 * ((1 - C) * K + ‖Z‖)) * ‖Y' - Y‖ +
        Real.exp (p * ‖Y' - Y‖) * p * ‖Y' - Y‖ * residualFraction p R Y := by
…

Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.residualFraction