GraphPathBaseline.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact dominant-path coordinates for the graph prediction

The distinguished diagonal carrier and scalar phase are removed explicitly. The graph prediction then has the path baseline used in §9, with constant path vector and residual denominator and an oscillating off-path numerator.

def OAI.LipschitzHilbert.graphPathVector line 28
def OAI.LipschitzHilbert.graphPathCoefficient line 31
def OAI.LipschitzHilbert.graphPathResidual line 34
def OAI.LipschitzHilbert.graphPathOffPath line 37
theorem OAI.LipschitzHilbert.phase_inverse_mul line 44

theorem OAI.LipschitzHilbert.graph_rotated_path_coefficient line 50

Source documentation

The path coefficient after its scalar phase has been removed.

theorem graph_rotated_path_coefficient (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    (lambda : ι → ℂ) (D p : ℝ) (i₀ : ι) (hl : 0 < l i₀) (hlambda : lambda i₀ ≠ 0) :
    (scalarPhase (lambda i₀))⁻¹ • predictionCoefficients l X lambda D p i₀ =
      graphPathCoefficient l lambda D p i₀ • graphPathVector l X p i₀ := by
…

Mentions: OAI.LipschitzHilbert.scalarPhase, OAI.LipschitzHilbert.predictionCoefficients, OAI.LipschitzHilbert.graphPathCoefficient, OAI.LipschitzHilbert.graphPathVector

theorem OAI.LipschitzHilbert.graph_path_denominator line 78

Source documentation

The child denominator splits into path energy and the off-path remainder.

theorem graph_path_denominator (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    {p : ℝ} (hp : 0 < p) (i₀ : ι) (hl : 0 ≤ l i₀) :
    1 + ∑ i, l i * ‖X i‖ ^ p =
      1 + ‖graphPathVector l X p i₀‖ ^ p + graphPathResidual l X p i₀ := by
…

Mentions: OAI.LipschitzHilbert.graphPathVector, OAI.LipschitzHilbert.graphPathResidual

theorem OAI.LipschitzHilbert.graph_prediction_path_baseline line 88

Source documentation

The graph-model prediction is exactly the dominant-path baseline.

theorem graph_prediction_path_baseline (frequency : ι → κ → ℝ) (l : ι → ℝ)
    (X : ι → EuclideanSpace ℂ κ) (lambda : ι → ℂ) (D : ℝ) {p : ℝ}
    (hp : 0 < p) (i₀ : ι) (hl : 0 < l i₀) (hlambda : lambda i₀ ≠ 0) (t : ℝ) :
    graphPredictionValue frequency l X lambda D p t =
      energyRatio p (1 + ‖graphPathVector l X p i₀‖ ^ p + graphPathResidual l X p i₀)
        (graphPathCoefficient l lambda D p i₀ • graphPathVector l X p i₀ +
          graphPathOffPath frequency l X lambda D p i₀ t) := by
…

Mentions: OAI.LipschitzHilbert.graphPredictionValue, OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.graphPathVector, OAI.LipschitzHilbert.graphPathResidual, OAI.LipschitzHilbert.graphPathCoefficient, OAI.LipschitzHilbert.graphPathOffPath

theorem OAI.LipschitzHilbert.graphPathResidual_nonneg line 112

theorem OAI.LipschitzHilbert.graphPathOffPath_norm_le line 117

Source documentation

The oscillating remainder retains the same off-path coefficient mass.

theorem graphPathOffPath_norm_le (frequency : ι → κ → ℝ) (l : ι → ℝ)
    (X : ι → EuclideanSpace ℂ κ) (lambda : ι → ℂ) (D p : ℝ) (i₀ : ι)
    (hlambda : lambda i₀ ≠ 0) (t : ℝ) :
    ‖graphPathOffPath frequency l X lambda D p i₀ t‖ ≤
      ∑ i : RemainderIndex i₀, ‖predictionCoefficients l X lambda D p i‖ := by
…

Mentions: OAI.LipschitzHilbert.graphPathOffPath, OAI.LipschitzHilbert.predictionCoefficients

theorem OAI.LipschitzHilbert.graphPathCoefficient_eq_pathCoefficient line 129

Source documentation

The coefficient is the real mass-fraction expression from the source when the modulus of the hierarchy weight is the expected power.

theorem graphPathCoefficient_eq_pathCoefficient (l : ι → ℝ) (lambda : ι → ℂ)
    (D p α r : ℝ) (i₀ : ι) (hp : p ≠ 0) (hrelation : p * phaseMu D p = α - 1)
    (hlambda : ‖lambda i₀‖ = r ^ phaseMu D p) :
    graphPathCoefficient l lambda D p i₀ =
      pathCoefficient (1 - α / p) (phaseMu D p) (l i₀) r := by
…

Mentions: OAI.LipschitzHilbert.graphPathCoefficient, OAI.LipschitzHilbert.pathCoefficient