GraphPhasePrediction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The mass-normalized node prediction

The explicitly constructed graph selection law and the diagonal Fourier gain bound the original parent/child ratio from §8, after the exact normalization identity. This is the normalized prediction estimate used in §9.

theorem OAI.LipschitzHilbert.diagonalModulation_smul line 28
theorem OAI.LipschitzHilbert.diagonalFourierSum_coefficients line 37

theorem OAI.LipschitzHilbert.diagonal_normalized_child_ratio line 45

Source documentation

The exact pointwise node/child normalization after diagonal modulation.

theorem diagonal_normalized_child_ratio (frequency : ι → κ → ℝ)
    (n : ℝ) (m : ι → ℝ) (A : ι → EuclideanSpace ℂ κ) (lambda : ι → ℂ)
    (μ α p t : ℝ) (hn : 0 < n) (hm : ∀ i, 0 < m i) (hrelation : p * μ = α - 1) :
    (n + n ^ (α - p) * ‖diagonalFourierSum frequency (fun i => lambda i • A i) t‖ ^ p) /
      (n + ∑ i, m i ^ (α - p) * ‖A i‖ ^ p) =
    (1 + ‖diagonalFourierSum frequency
      (fun i => ((((m i / n) ^ (1 - μ) : ℝ) : ℂ) * lambda i) •
        (((m i ^ (μ - 1) : ℝ) : ℂ) • A i)) t‖ ^ p) /
      (1 + ∑ i, (m i / n) * ‖((m i ^ (μ - 1) : ℝ) : ℂ) • A i‖ ^ p) := by
…

theorem OAI.LipschitzHilbert.graph_node_prediction_average line 71

Source documentation

The graph assumptions and original child masses imply the actual ratio average is at most one, with no selection-law hypothesis.

theorem graph_node_prediction_average
    (G : ι → ι → Prop) (hG : ∀ ⦃i j⦄, G i j → G j i)
    (w m : ι → ℝ) (n : ℝ) (hw : ∀ i, 0 < w i) (hn : 0 < n)
    (hm : ∀ i, orderMass w (closedNeighborhood G i) ≤ m i)
    (hchildren : ∑ i, w i ≤ n)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → κ → ℝ)
    (A : ι → EuclideanSpace ℂ κ) (lambda : ι → ℂ)
    {gap D p α : ℝ} (hgap : 0 < gap) (hν : FourierGap ν gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hrelation : p * phaseMu D p = α - 1)
    (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)
    (hlambda : ∀ i, ‖lambda i‖ ≤ (w i / m i) ^ phaseMu D p) :
…

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