LogEnergyGradient.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Uniform Lipschitz bound for the logarithmic-energy derivative

The dimension-free derivative bound from §9 is proved using the radial coefficient and its one-dimensional derivative. It supplies the cancellation between the path numerator and denominator when the path child is dominant.

def OAI.LipschitzHilbert.radialLogSlope line 19
Source documentation
The radial size of the logarithmic-energy gradient.
```
def radialLogSlope (p r : ℝ) : ℝ := p * r ^ (p - 1) / (1 + r ^ p)
```
def OAI.LipschitzHilbert.radialLogCoefficient line 22
Source documentation
The scalar coefficient multiplying the path vector in the derivative.
```
def radialLogCoefficient (p r : ℝ) : ℝ := p * r ^ (p - 2) / (1 + r ^ p)
```
theorem OAI.LipschitzHilbert.rpow_lower_exponent_le_one_add line 24
theorem OAI.LipschitzHilbert.radialLogCoefficient_nonneg line 31
theorem OAI.LipschitzHilbert.radialLogCoefficient_le line 36
theorem OAI.LipschitzHilbert.radialLogCoefficient_mul line 44
theorem OAI.LipschitzHilbert.hasDerivAt_radialLogSlope line 53
theorem OAI.LipschitzHilbert.radialLogSlope_derivative_bound line 66
theorem OAI.LipschitzHilbert.radialLogSlope_lipschitz line 90

theorem OAI.LipschitzHilbert.radial_vector_lipschitz line 103

Source documentation

A bounded radial coefficient whose radial size is Lipschitz gives a Lipschitz radial vector field. This proof never divides by a vector norm.

theorem radial_vector_lipschitz (k : ℝ → ℝ) {C L : ℝ}
    (hC : 0 ≤ C) (hL : 0 ≤ L)
    (hk : ∀ r, 0 ≤ r → |k r| ≤ C)
    (hsize : ∀ r s, 0 ≤ r → 0 ≤ s → |k r * r - k s * s| ≤ L * |r - s|)
    (x y : E) : ‖k ‖x‖ • x - k ‖y‖ • y‖ ≤ (L + 2 * C) * ‖x - y‖ := by
…

def OAI.LipschitzHilbert.logEnergyDerivative line 142
Source documentation
The derivative of logarithmic energy as an actual bounded linear functional.
```
def logEnergyDerivative (p : ℝ) (x : E) : E →L[ℝ] ℝ :=
…
```
theorem OAI.LipschitzHilbert.hasFDerivAt_logEnergy line 145
theorem OAI.LipschitzHilbert.norm_logEnergyDerivative_le line 156
Source documentation
The first derivative has the sharp global bound p.
```
theorem norm_logEnergyDerivative_le {p : ℝ} (hp : 2 ≤ p) (x : E) :
    ‖logEnergyDerivative p x‖ ≤ p := by
…
```
Mentions: OAI.LipschitzHilbert.logEnergyDerivative
theorem OAI.LipschitzHilbert.logEnergyDerivative_lipschitz line 167
Source documentation
The global derivative is Lipschitz with a dimension-free 4 p² constant.
```
theorem logEnergyDerivative_lipschitz {p : ℝ} (hp : 4 ≤ p) (x y : E) :
    ‖logEnergyDerivative p x - logEnergyDerivative p y‖ ≤ 4 * p ^ 2 * ‖x - y‖ := by
…
```
Mentions: OAI.LipschitzHilbert.logEnergyDerivative