UnaryEnergy.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Unary residual energies

The amount is the actual vertexAmount from §11. Its logarithmic motion and the small correction log(1+h/V) are the analytic ingredients of the unary-segment telescope in §10, equation src-28.

theorem OAI.LipschitzHilbert.vertexAmount_pos line 21
theorem OAI.LipschitzHilbert.mass_le_vertexAmount line 27
theorem OAI.LipschitzHilbert.vertexAmount_eq_normalized line 33
Source documentation
Here mu=(a-1)/p, so this is exactly the normalization used in §10.
```
theorem vertexAmount_eq_normalized {n a p : ℝ} (hn : 0 < n) (hp : p ≠ 0) (A : E) :
    vertexAmount n A a p = n * (1 + ‖(n ^ ((a - 1) / p - 1)) • A‖ ^ p) := by
…
```
Mentions: OAI.LipschitzHilbert.vertexAmount
theorem OAI.LipschitzHilbert.log_vertexAmount_eq line 44
theorem OAI.LipschitzHilbert.log_vertexAmount_lipschitz line 51
theorem OAI.LipschitzHilbert.vertexAmount_subsolution line 65
Source documentation
Increasing the mass and contracting the amplitude makes the amount a subsolution, apart from the exact mass drop.
```
theorem vertexAmount_subsolution {n n' a p : ℝ} (hn' : 0 < n') (hn : n' ≤ n)
    (hap : a ≤ p) (hp : 0 ≤ p) (A A' : E) (hA : ‖A‖ ≤ ‖A'‖) :
    vertexAmount n A a p ≤ (n - n') + vertexAmount n' A' a p := by
…
```
Mentions: OAI.LipschitzHilbert.vertexAmount
def OAI.LipschitzHilbert.logCorrection line 78
theorem OAI.LipschitzHilbert.hasDerivAt_logCorrection line 80
theorem OAI.LipschitzHilbert.logCorrection_derivative_bound line 91
theorem OAI.LipschitzHilbert.logCorrection_log line 101

theorem OAI.LipschitzHilbert.log_correction_lipschitz line 110

Source documentation

The residual denominator correction has Lipschitz constant h/n in logarithmic coordinates whenever both amounts are at least n.

theorem log_correction_lipschitz {h n V W : ℝ} (hh : 0 ≤ h) (hn : 0 < n)
    (hV : n ≤ V) (hW : n ≤ W) :
    |Real.log (1 + h / V) - Real.log (1 + h / W)| ≤
      (h / n) * |Real.log V - Real.log W| := by
…