SourceNodeRatio.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The normalized prediction is exactly the source node ratio with its packet residual removed. The denominator retains the stopped-top mass and every nonempty eligible child, including zero-amplitude children.

def OAI.LipschitzHilbert.sourceNodeDenominator line 18
def OAI.LipschitzHilbert.sourceNodeRatio line 21
theorem OAI.LipschitzHilbert.sourceNodeDenominator_stopped_mass line 25
theorem OAI.LipschitzHilbert.sourceNodeDenominator_pos line 31
theorem OAI.LipschitzHilbert.sourceNodeRatio_pos line 38

theorem OAI.LipschitzHilbert.sourcePredictionValue_eq_nodeRatio line 45

Source documentation

Exact source equation (src-25), in the actual prediction notation.

theorem sourcePredictionValue_eq_nodeRatio (n : ℝ) (c : ι → ℝ)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ) (μ α p : ℝ)
    (hn : 0 < n) (hc : ∀ i, 0 < c i) (hrelation : p*μ = α-1) :
    sourcePredictionValue p μ n c A lam =
      sourceNodeRatio n c A α p (∑ i, lam i • A i) := by
…

Mentions: OAI.LipschitzHilbert.sourcePredictionValue, OAI.LipschitzHilbert.sourceNodeRatio

theorem OAI.LipschitzHilbert.sourcePredictionValue_eq_residual_free_ratio line 57

Source documentation

Removing a residual is literal subtraction in the parent amplitude, with the child denominator left unchanged.

theorem sourcePredictionValue_eq_residual_free_ratio
    (n : ℝ) (c : ι → ℝ) (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
    (parentAmplitude residual : EuclideanSpace ℂ κ) (μ α p : ℝ)
    (hn : 0 < n) (hc : ∀ i, 0 < c i) (hrelation : p*μ = α-1)
    (hdecomp : parentAmplitude = residual+∑ i, lam i • A i) :
    sourcePredictionValue p μ n c A lam =
      sourceNodeRatio n c A α p (parentAmplitude-residual) := by
…

Mentions: OAI.LipschitzHilbert.sourcePredictionValue, OAI.LipschitzHilbert.sourceNodeRatio

theorem OAI.LipschitzHilbert.source_node_log_residual_error line 69

Source documentation

The source residual logarithmic error, with its exact mass power. The common child denominator cancels before applying the energy estimate.

theorem source_node_log_residual_error
    (n : ℝ) (c : ι → ℝ) (A : ι → EuclideanSpace ℂ κ)
    (parentAmplitude residual : EuclideanSpace ℂ κ) (μ α p : ℝ)
    (hn : 0 < n) (hc : ∀ i, 0 ≤ c i) (hp : 1 ≤ p) (hrelation : p*μ = α-1) :
    |Real.log (sourceNodeRatio n c A α p parentAmplitude)-
        Real.log (sourceNodeRatio n c A α p (parentAmplitude-residual))| ≤
      p*n^(μ-1)*‖residual‖ := by
…

Mentions: OAI.LipschitzHilbert.sourceNodeRatio

theorem OAI.LipschitzHilbert.source_node_log_prediction_error line 87

theorem OAI.LipschitzHilbert.AngularGrid.source_block_residual_free_ratio line 106

Source documentation

On an actual source block, the normalized predictor is exactly beta0: the node amount with its literal packet residual removed, divided by the original stopped-mass/child-amount denominator.

theorem source_block_residual_free_ratio {τ σ X : Type*}
    (g : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (weight : τ → X → ℝ) (hprecision : ∀ t ∈ tops, 0 ≤ precision t)
    (hweight : ∀ t x, 0 < weight t x) (K : ℕ) (gap : ℕ → ℝ)
    (packets : Finset σ) (assigned : σ → τ) (stop : σ → ℕ)
    (value : σ → EuclideanSpace ℂ κ) (phase : ℕ → ℂ) (a : ℝ) (x : X)
    (hassigned : ∀ s ∈ packets, assigned s ∈ tops)
    (heligible : ∀ s ∈ packets, g.eligible cutoff (precision (assigned s)) (stop s))
    {lower upper : ℕ} (hle : lower ≤ upper) (parent : ℤ)
    (hparent : (g.cellTops tops slope precision cutoff lower parent).Nonempty)
    (μ α p : ℝ) (hrelation : p*μ = α-1) :
    let cells := g.sourceBlockCells tops slope precision cutoff lower upper parent
…

Mentions: OAI.LipschitzHilbert.AngularGrid