SourceEmptyPrediction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A block with no continuing eligible-top child has prediction one. It does not require selecting a fictitious child for the graph argument.

theorem OAI.LipschitzHilbert.source_empty_prediction line 13

theorem OAI.LipschitzHilbert.source_empty_grid_prediction line 21

Source documentation

The same normalized local factor API covers an empty continuing family, even when the distinguished path has ended.

theorem source_empty_grid_prediction {ι κ : Type} [Fintype ι] [IsEmpty ι] [Fintype κ]
    (grid : FiniteLineGrid) (level : ℕ) (p μ e : ℝ) (hp : 0 < p) (he : 0 ≤ e)
    (n : ℝ → ℝ) (c : ℝ → ι → ℝ) (A : ℝ → ι → EuclideanSpace ℂ κ)
    (lam : ℝ → ι → ℂ) :
    ∃ Γ : ℝ → ℝ, Measurable Γ ∧
      Integrable Γ (intervalProbability grid.origin (grid.origin+grid.width)) ∧
      (∀ b, 0 ≤ Γ b) ∧
      (∫ b, Γ b ∂intervalProbability grid.origin (grid.origin+grid.width)) ≤ 1 ∧
      (∀ b d, grid.index level b = grid.index level d → Γ b = Γ d) ∧
      ∀ b ∈ grid.root, sourcePredictionValue p μ (n b) (c b) (A b) (lam b) ≤ Real.exp e*Γ b := by
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.intervalProbability, OAI.LipschitzHilbert.sourcePredictionValue