PredictionCells.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Measurable step-supremum prediction factors

Inside one root cell, a finite measurable partition gives an explicit step supremum. Logarithmic cell oscillation controls its normalization, producing the actual nonnegative, measurable, average-one factor.

def OAI.LipschitzHilbert.predictionCell line 24
Source documentation
A finer cell, restricted to the current root region.
```
def predictionCell (I : Set α) (P : α → κ) (i : κ) : Set α := {x | x ∈ I ∧ P x = i}
```
def OAI.LipschitzHilbert.predictionStepSup line 27
Source documentation
Actual cell supremums, constant on the finer partition.
```
def predictionStepSup (B : α → ℝ) (I : Set α) (P : α → κ) (x : α) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.predictionStepSup_constant line 31
theorem OAI.LipschitzHilbert.measurable_finite_profile line 35
theorem OAI.LipschitzHilbert.measurable_predictionStepSup line 51
theorem OAI.LipschitzHilbert.integrable_predictionStepSup line 55
theorem OAI.LipschitzHilbert.predictionStepSup_bounds line 61
theorem OAI.LipschitzHilbert.predictionStepSup_nonnegative line 70

theorem OAI.LipschitzHilbert.exists_normalized_prediction_steps line 88

Source documentation

Construct the normalized step factor explicitly, including measurability, constancy on finer cells, integral at most one, and the pointwise comparison.

theorem exists_normalized_prediction_steps (μ : Measure α) [IsProbabilityMeasure μ]
    (B : α → ℝ) (I : Set α) (P : α → κ)
    (hP : ∀ i, MeasurableSet {x | P x = i}) (hsupport : ∀ᵐ x ∂μ, x ∈ I)
    (hpositive : ∀ x ∈ I, 0 < B x) (hB : Integrable B μ)
    {a b u : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hu : 0 ≤ u)
    (haverage : ∫ x, B x ∂μ ≤ 1 + a * u)
    (hosc : ∀ x ∈ I, ∀ y ∈ I, P y = P x → |Real.log (B y) - Real.log (B x)| ≤ b * u) :
    ∃ Γ : α → ℝ, Measurable Γ ∧ Integrable Γ μ ∧ (∀ x, 0 ≤ Γ x) ∧
      (∫ x, Γ x ∂μ) ≤ 1 ∧ (∀ x y, P x = P y → Γ x = Γ y) ∧
      ∀ x ∈ I, B x ≤ Real.exp ((a + b) * u) * Γ x := by
…