GraphPredictionFactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A constructed step factor for the graph prediction

For the fixed snapshot model of §9, combine graph selection, carrier removal, probability-mixture transfer, finite-cell supremums, and exact normalization. The resulting factor is an actual measurable step function of average at most one. Every loss in its comparison retains the off-path mass parameter u.

def OAI.LipschitzHilbert.predictionCoefficients line 28
def OAI.LipschitzHilbert.graphPredictionValue line 32
theorem OAI.LipschitzHilbert.positive_blend line 38

theorem OAI.LipschitzHilbert.graph_prediction_step_factor line 47

Source documentation

The finite-snapshot graph prediction admits a measurable normalized step factor, with only a relative off-path-mass loss in its pointwise comparison.

theorem graph_prediction_step_factor
    (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 ω] [IsProbabilityMeasure τ]
    (frequency : ι → κ → ℝ) (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    (lambda : ι → ℂ) (i₀ : ι) (I : Set ℝ) (P : ℝ → σ)
    {η gap D p K u L H θ : ℝ}
    (hη0 : 0 ≤ η) (hη1 : η < 1) (hgap : 0 < gap)
    (hν : FourierGap (predictionMixture ω τ η) gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hfrequency : ∀ i j, i ≠ j → ¬G i j → ∀ k, gap ≤ |frequency i k - frequency j k|)
    (hcard : ∀ S : Finset ι, (S : Set ι).Pairwise (fun i j => ¬G i j) → (S.card : ℝ) ≤ D)
…

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