PredictionNormalization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

From probability averages to normalized prediction steps

The probability-mixture transfer, step supremum control, and normalization costs used in §9. All averages below are actual Bochner integrals.

theorem OAI.LipschitzHilbert.probability_mixture_average_le line 24

Source documentation

Transfer from the band-limited mixture to its principal probability. The loss is proportional to the lower deviation of the prediction.

theorem probability_mixture_average_le (ω τ : Measure α)
    [IsProbabilityMeasure ω] [IsProbabilityMeasure τ] (B : α → ℝ)
    {η ε : ℝ} (hη0 : 0 ≤ η) (hη1 : η < 1)
    (hω : Integrable B ω) (hτ : Integrable B τ)
    (hlower : ∀ᵐ x ∂τ, 1 - ε ≤ B x)
    (haverage : (∫ x, B x ∂(ENNReal.ofReal (1 - η) • ω + ENNReal.ofReal η • τ)) ≤ 1) :
    (∫ x, B x ∂ω) ≤ 1 + η / (1 - η) * ε := by
…

theorem OAI.LipschitzHilbert.blend_average_and_lower line 48

Source documentation

Blending with the constant one preserves an upper average and shrinks pointwise lower deviations by the exact blend factor.

theorem blend_average_and_lower (ν : Measure α) [IsProbabilityMeasure ν]
    (B : α → ℝ) {θ ε : ℝ} (hθ1 : θ ≤ 1)
    (hB : Integrable B ν) (haverage : ∫ x, B x ∂ν ≤ 1)
    (hlower : ∀ x, 1 - ε ≤ B x) :
    (∫ x, ((1 - θ) * B x + θ) ∂ν) ≤ 1 ∧
      ∀ x, 1 - (1 - θ) * ε ≤ (1 - θ) * B x + θ := by
…

def OAI.LipschitzHilbert.predictionCellSup line 62
Source documentation
Supremum on one step cell.
```
def predictionCellSup (B : α → ℝ) (I : Set α) : ℝ := sSup (B '' I)
…
```

theorem OAI.LipschitzHilbert.prediction_cell_sup_bounds line 67

Source documentation

A log-oscillation bound gives the precise multiplicative cell-supremum bound. It also proves the relevant supremum is finite.

theorem prediction_cell_sup_bounds (B : α → ℝ) (I : Set α) {x : α} (hx : x ∈ I)
    (hpositive : ∀ y ∈ I, 0 < B y) {c : ℝ}
    (hosc : ∀ y ∈ I, |Real.log (B y) - Real.log (B x)| ≤ c) :
    B x ≤ predictionCellSup B I ∧ predictionCellSup B I ≤ Real.exp c * B x := by
…

Mentions: OAI.LipschitzHilbert.predictionCellSup

def OAI.LipschitzHilbert.predictionNormalizer line 85
Source documentation
The normalization denominator from §9.
```
def predictionNormalizer (ν : Measure α) (Bsharp : α → ℝ) : ℝ :=
…
```
def OAI.LipschitzHilbert.normalizedPrediction line 89
Source documentation
The normalized step prediction.
```
def normalizedPrediction (ν : Measure α) (Bsharp : α → ℝ) (x : α) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.predictionNormalizer_pos line 92
theorem OAI.LipschitzHilbert.normalizedPrediction_nonnegative line 96
theorem OAI.LipschitzHilbert.normalizedPrediction_average_le_one line 100
theorem OAI.LipschitzHilbert.predictionNormalizer_log_le line 105

theorem OAI.LipschitzHilbert.step_normalization_cost line 113

Source documentation

Exponential step oscillation and an additive average error yield an additive logarithmic normalization cost.

theorem step_normalization_cost (ν : Measure α)
    (B Bsharp : α → ℝ) {a b u : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hu : 0 ≤ u)
    (hB : Integrable B ν) (hsharp : Integrable Bsharp ν)
    (hmajorant : ∀ᵐ x ∂ν, Bsharp x ≤ Real.exp (b * u) * B x)
    (haverage : ∫ x, B x ∂ν ≤ 1 + a * u) :
    Real.log (predictionNormalizer ν Bsharp) ≤ (a + b) * u := by
…

Mentions: OAI.LipschitzHilbert.predictionNormalizer

theorem OAI.LipschitzHilbert.prediction_domination_after_normalization line 132

Source documentation

The pointwise comparison survives step majorization and normalization, with the logarithmic normalization cost added to its exponent.

theorem prediction_domination_after_normalization (ν : Measure α)
    (B Bsharp β : α → ℝ) {a c u : ℝ}
    (hsharp : ∀ x, B x ≤ Bsharp x) (hsharp0 : ∀ x, 0 ≤ Bsharp x)
    (hcomparison : ∀ x, β x ≤ Real.exp (a * u) * B x)
    (hcost : Real.log (predictionNormalizer ν Bsharp) ≤ c * u) (x : α) :
    β x ≤ Real.exp ((a + c) * u) * normalizedPrediction ν Bsharp x := by
…

Mentions: OAI.LipschitzHilbert.predictionNormalizer, OAI.LipschitzHilbert.normalizedPrediction