LineGridPrediction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The snapshot prediction factor on the actual finite line-cell mesh.

theorem OAI.LipschitzHilbert.intervalProbability_ae_mem_Ico line 20

theorem OAI.LipschitzHilbert.FiniteLineGrid.graph_prediction_step line 38

Source documentation

Apply the constructed graph predictor to a finite uniform line grid. There is no free measurable partition or cell-diameter hypothesis here.

theorem graph_prediction_step {ι κ : Type*} [Fintype ι] [Fintype κ]
    (grid : FiniteLineGrid) (level : ℕ) (hlevel : level ≤ grid.depth)
    (G : ι → ι → Prop) (hG : ∀ ⦃i j⦄, G i j → G j i)
    (w m : ι → ℝ) (hw : ∀ i, 0 < w i)
    (hm : ∀ i, orderMass w (closedNeighborhood G i) ≤ m i)
    (τ : Measure ℝ) [IsProbabilityMeasure τ]
    (frequency : ι → κ → ℝ) (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    (lambda : ι → ℂ) (i₀ : ι)
    {η gap D p K u freqBound θ : ℝ}
    (hη0 : 0 ≤ η) (hη1 : η < 1) (hgap : 0 < gap)
    (hν : FourierGap (predictionMixture
      (intervalProbability grid.origin (grid.origin + grid.width)) τ η) gap)
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.orderMass, OAI.LipschitzHilbert.closedNeighborhood, OAI.LipschitzHilbert.predictionMixture, OAI.LipschitzHilbert.intervalProbability