LogEnergy.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic energy and relative prediction deficits

The exact p-Lipschitz estimate for log (1 + ‖x‖^p) from §§9–10. A fixed denominator then cancels from differences of log predictions, so bounded off-path motion gives a deficit proportional to the path drop.

def OAI.LipschitzHilbert.logEnergy line 21
theorem OAI.LipschitzHilbert.rpow_predecessor_le_one_add line 23
theorem OAI.LipschitzHilbert.hasDerivAt_scalar_logEnergy line 31
theorem OAI.LipschitzHilbert.scalar_logEnergy_derivative_bound line 37
theorem OAI.LipschitzHilbert.scalar_logEnergy_lipschitz line 44
theorem OAI.LipschitzHilbert.logEnergy_lipschitz line 53
Source documentation
The exact global logarithmic-energy Lipschitz estimate, requiring only that the vectors lie in a normed additive group.
```
theorem logEnergy_lipschitz {p : ℝ} (hp : 1 ≤ p) (x y : E) :
    |logEnergy p x - logEnergy p y| ≤ p * ‖x - y‖ := by
…
```
Mentions: OAI.LipschitzHilbert.logEnergy
def OAI.LipschitzHilbert.energyRatio line 59
Source documentation
The prediction ratio with a fixed positive denominator.
```
def energyRatio (p denominator : ℝ) (x : E) : ℝ := (1 + ‖x‖ ^ p) / denominator
```
theorem OAI.LipschitzHilbert.energyRatio_pos line 61
theorem OAI.LipschitzHilbert.log_energyRatio_sub line 64
theorem OAI.LipschitzHilbert.log_energyRatio_lipschitz line 72
theorem OAI.LipschitzHilbert.energyRatio_deficit_of_exceeds_one line 81
Source documentation
A value exceeding one and a bound on numerator motion force a pointwise lower bound with the same motion factor. The fixed denominator is unrestricted.
```
theorem energyRatio_deficit_of_exceeds_one {p denominator M : ℝ}
    (hp : 1 ≤ p) (hd : 0 < denominator) (hM : 0 ≤ M) (x y : E)
    (hy : 1 < energyRatio p denominator y) (hmotion : ‖x - y‖ ≤ M) :
    max (1 - energyRatio p denominator x) 0 ≤ p * M := by
…
```
Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.fixed_path_prediction_deficit line 96

Source documentation

For a fixed path vector, off-path vectors of size at most B have diameter at most 2B; hence a model prediction exceeding one has deficit at most 2pB.

theorem fixed_path_prediction_deficit {T : Type*} {p denominator B : ℝ}
    (hp : 1 ≤ p) (hd : 0 < denominator) (hB : 0 ≤ B)
    (Y : E) (Z : T → E) (hZ : ∀ t, ‖Z t‖ ≤ B)
    (hexceeds : ∃ t, 1 < energyRatio p denominator (Y + Z t)) (t : T) :
    max (1 - energyRatio p denominator (Y + Z t)) 0 ≤ 2 * p * B := by
…

Mentions: OAI.LipschitzHilbert.energyRatio