SourcePredictionValues.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The source node ratio and its snapshot graph predictor, with the original child amplitudes and masses kept explicit.

def OAI.LipschitzHilbert.sourcePredictionValue line 17
Source documentation
The exact source prediction in mass-normalized child variables.
```
def sourcePredictionValue (p μ n : ℝ) (c : ι → ℝ)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ) : ℝ :=
…
```

def OAI.LipschitzHilbert.sourceSnapshotPrediction line 23

Source documentation

The same snapshot, with only its prescribed diagonal carriers moving.

def sourceSnapshotPrediction (p μ n : ℝ) (c : ι → ℝ)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ) (frequency : ι → κ → ℝ) (b : ℝ) : ℝ :=
…

theorem OAI.LipschitzHilbert.source_prediction_numerator_identity line 29

theorem OAI.LipschitzHilbert.source_snapshot_graph_identity line 39

Source documentation

The graph averaging theorem applies to exactly the source snapshot.

theorem source_snapshot_graph_identity (p D n : ℝ) (c : ι → ℝ)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ) (frequency : ι → κ → ℝ) (b : ℝ) :
    sourceSnapshotPrediction p (phaseMu D p) n c A lam frequency b =
      graphPredictionValue frequency (fun i => c i/n)
        (fun i => (c i)^(phaseMu D p-1) • A i) lam D p b := by
…

Mentions: OAI.LipschitzHilbert.sourceSnapshotPrediction, OAI.LipschitzHilbert.graphPredictionValue

theorem OAI.LipschitzHilbert.source_snapshot_graph_coefficient_sum line 50

Source documentation

The coefficient sum used by the line-grid theorem follows from the original amplitudes and actual child fractions, including after shrinkage.

theorem source_snapshot_graph_coefficient_sum {p D n ε C K u : ℝ}
    (hn : 0 < n) (hε : 0 ≤ ε) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (hsize : C*n^(phaseMu D p) ≤ K)
    (c : ι → ℝ) (hc : ∀ i, 0 < c i)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
    (hA : ∀ i, ‖A i‖ ≤ C*c i) (hlam : ∀ i, ‖lam i‖ ≤ 1)
    (hmass : ∑ i, c i/n ≤ u) :
    (∑ i, ‖predictionCoefficients (fun i => c i/n)
      (fun i => (c i)^(phaseMu D p-1) • radialShrink (2*ε*c i) (A i)) lam D p i‖) ≤ K*u := by
…

Mentions: OAI.LipschitzHilbert.predictionCoefficients, OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.source_balanced_values_blend line 74

Source documentation

The shrunken source comparison in the value notation used for assembly.

theorem source_balanced_values_blend
    {n n' p μ ε K u C θ : ℝ} (hn : 0 < n) (hn' : 0 < n')
    (c c' : ι → ℝ) (hc : ∀ i, 0 < c i) (hc' : ∀ i, 0 < c' i)
    (hp : 1 ≤ p) (hε : 0 ≤ ε) (hK : 0 ≤ K) (hpower : n^μ ≤ K)
    (hu : 1/2 ≤ u) (hsum : ∑ i, c i/n ≤ 1)
    (frequency : ι → κ → ℝ) (b : ℝ)
    (A A' : ι → EuclideanSpace ℂ κ) (lam lam' : ι → ℂ)
    (hlam : ∀ i, ‖lam i‖ ≤ 1)
    (hscaled : ∀ i,
      ‖massPowerScale n' (c' i) (-(1/p)) (μ-1+1/p) • A' i-
        diagonalModulation (frequency i)
          (massPowerScale n (c i) (-(1/p)) (μ-1+1/p) • A i) b‖ ≤
…

Mentions: OAI.LipschitzHilbert.massPowerScale