RadialShrink.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Radial snapshot shrinkage and the balanced prediction comparison

Section 9 shrinks each snapshot amplitude radially by a controlled distance. The exact norm formula makes its denominator smaller than every nearby moved denominator. The numerator motion and the logarithmic-energy Lipschitz bound then give the balanced-case comparison, with its relative path-drop factor.

def OAI.LipschitzHilbert.radialShrink line 25
Source documentation
Radial truncation by the distance δ; its value at the zero vector is zero.
```
def radialShrink (δ : ℝ) (x : E) : E := max (1 - δ / ‖x‖) 0 • x
```
theorem OAI.LipschitzHilbert.radialShrink_zero line 27
theorem OAI.LipschitzHilbert.norm_radialShrink line 31
Source documentation
The radial truncation removes exactly the smaller of δ and the norm.
```
theorem norm_radialShrink {δ : ℝ} (hδ : 0 ≤ δ) (x : E) :
    ‖radialShrink δ x‖ = max (‖x‖ - δ) 0 := by
…
```
Mentions: OAI.LipschitzHilbert.radialShrink
theorem OAI.LipschitzHilbert.radialShrink_eq_zero_iff line 49
Source documentation
Vectors already within the discarded radius are suppressed completely.
```
theorem radialShrink_eq_zero_iff {δ : ℝ} (hδ : 0 ≤ δ) (x : E) :
    radialShrink δ x = 0 ↔ ‖x‖ ≤ δ := by
…
```
Mentions: OAI.LipschitzHilbert.radialShrink
theorem OAI.LipschitzHilbert.norm_radialShrink_le line 60
theorem OAI.LipschitzHilbert.norm_radialShrink_sub_le line 66
Source documentation
The change in the amplitude never exceeds the requested shrinkage distance.
```
theorem norm_radialShrink_sub_le {δ : ℝ} (hδ : 0 ≤ δ) (x : E) :
    ‖radialShrink δ x - x‖ ≤ δ := by
…
```
Mentions: OAI.LipschitzHilbert.radialShrink
theorem OAI.LipschitzHilbert.scaled_radialShrink_norm_le_of_error line 82
Source documentation
A nearby moved vector has norm at least the scaled, radially shrunken snapshot. z allows an arbitrary norm-preserving rotation of the snapshot.
```
theorem scaled_radialShrink_norm_le_of_error {δ c : ℝ} (hδ : 0 ≤ δ) (hc : 0 ≤ c)
    (x y z : E) (hz : ‖z‖ = c * ‖x‖) (hmotion : ‖y - z‖ ≤ c * δ) :
    ‖c • radialShrink δ x‖ ≤ ‖y‖ := by
…
```
Mentions: OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.scaled_radialShrink_power_le_of_error line 97

Source documentation

Raising the denominator comparison to any nonnegative real power preserves it.

theorem scaled_radialShrink_power_le_of_error {δ c p : ℝ}
    (hδ : 0 ≤ δ) (hc : 0 ≤ c) (hp : 0 ≤ p)
    (x y z : E) (hz : ‖z‖ = c * ‖x‖) (hmotion : ‖y - z‖ ≤ c * δ) :
    ‖c • radialShrink δ x‖ ^ p ≤ ‖y‖ ^ p :=
…

Mentions: OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.norm_weighted_smul_rpow line 103

theorem OAI.LipschitzHilbert.weighted_radialShrink_power_le_of_error line 111

Source documentation

The exact weighted denominator comparison from pred:denominator-lower-bound. The permitted motion is measured after the positive l^(1/p) rescaling.

theorem weighted_radialShrink_power_le_of_error {δ p l l' : ℝ}
    (hδ : 0 ≤ δ) (hp : 0 < p) (hl : 0 ≤ l) (hl' : 0 ≤ l')
    (x y z : E) (hz : ‖z‖ = l ^ (1 / p) * ‖x‖)
    (hmotion : ‖l' ^ (1 / p) • y - z‖ ≤ l ^ (1 / p) * δ) :
    l * ‖radialShrink δ x‖ ^ p ≤ l' * ‖y‖ ^ p := by
…

Mentions: OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.prediction_log_comparison line 123

Source documentation

With the model denominator below the actual denominator, only numerator motion contributes positively to the logarithmic ratio comparison.

theorem prediction_log_comparison {p dActual dModel : ℝ} (hp : 1 ≤ p)
    (hdModel : 0 < dModel) (hden : dModel ≤ dActual) (actual model : E) :
    Real.log (energyRatio p dActual actual) - Real.log (energyRatio p dModel model) ≤
      p * ‖actual - model‖ := by
…

Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.balanced_prediction_log_comparison line 141

Source documentation

The balanced case of pred:balanced-comparison. Each child contributes ε K lᵢ to numerator motion, the weights have total mass at most one, and u ≥ 1/2 recovers the relative path-drop factor at the cost of exactly two.

theorem balanced_prediction_log_comparison
    {p dActual dModel ε K u : ℝ} (hp : 1 ≤ p)
    (hdModel : 0 < dModel) (hden : dModel ≤ dActual)
    (hε : 0 ≤ ε) (hK : 0 ≤ K) (hu : 1 / 2 ≤ u)
    (l : ι → ℝ) (hsum : ∑ i, l i ≤ 1)
    (actual model : ι → E) (hmotion : ∀ i, ‖actual i - model i‖ ≤ ε * K * l i) :
    Real.log (energyRatio p dActual (∑ i, actual i)) -
      Real.log (energyRatio p dModel (∑ i, model i)) ≤ 2 * p * ε * K * u := by
…

Mentions: OAI.LipschitzHilbert.energyRatio

theorem OAI.LipschitzHilbert.weighted_radialShrink_denominator_le_of_error line 163

Source documentation

Summing the individual shrinkage comparisons produces the actual one-sided child denominator bound, including its constant term.

theorem weighted_radialShrink_denominator_le_of_error {p : ℝ} (hp : 0 < p)
    (δ l l' : ι → ℝ) (hδ : ∀ i, 0 ≤ δ i) (hl : ∀ i, 0 ≤ l i)
    (hl' : ∀ i, 0 ≤ l' i) (x y z : ι → E)
    (hz : ∀ i, ‖z i‖ = l i ^ (1 / p) * ‖x i‖)
    (hmotion : ∀ i, ‖l' i ^ (1 / p) • y i - z i‖ ≤ l i ^ (1 / p) * δ i) :
    1 + ∑ i, l i * ‖radialShrink (δ i) (x i)‖ ^ p ≤
      1 + ∑ i, l' i * ‖y i‖ ^ p := by
…

Mentions: OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.balanced_radial_prediction_log_comparison line 177

Source documentation

The balanced snapshot comparison with the denominator ordering discharged by radial shrinkage rather than supplied as a separate analytic assumption.

theorem balanced_radial_prediction_log_comparison
    {p ε K u : ℝ} (hp : 1 ≤ p) (hε : 0 ≤ ε) (hK : 0 ≤ K) (hu : 1 / 2 ≤ u)
    (δ l l' : ι → ℝ) (hδ : ∀ i, 0 ≤ δ i) (hl : ∀ i, 0 ≤ l i)
    (hl' : ∀ i, 0 ≤ l' i) (hsum : ∑ i, l i ≤ 1)
    (x y z actual model : ι → E)
    (hz : ∀ i, ‖z i‖ = l i ^ (1 / p) * ‖x i‖)
    (hscaledMotion : ∀ i, ‖l' i ^ (1 / p) • y i - z i‖ ≤ l i ^ (1 / p) * δ i)
    (hnumeratorMotion : ∀ i, ‖actual i - model i‖ ≤ ε * K * l i) :
    Real.log (energyRatio p (1 + ∑ i, l' i * ‖y i‖ ^ p) (∑ i, actual i)) -
      Real.log (energyRatio p (1 + ∑ i, l i * ‖radialShrink (δ i) (x i)‖ ^ p)
        (∑ i, model i)) ≤ 2 * p * ε * K * u := by
…

Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.radialShrink