SourceBalancedPrediction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The balanced branch of §9 for actual mass-normalized child amplitudes. The one-sided denominator comparison is derived from scaled amplitude motion, and the numerator uses the original child-mass error budget.

theorem OAI.LipschitzHilbert.source_normalized_numerator_eq line 15
theorem OAI.LipschitzHilbert.source_normalized_modulated_numerator_eq line 31

theorem OAI.LipschitzHilbert.source_prediction_denominator_sum_shrink line 44

Source documentation

Each child's actual radial shrink gives the summed denominator ordering, without an additional denominator hypothesis.

theorem source_prediction_denominator_sum_shrink
    {n n' p μ ε : ℝ} (hn : 0 < n) (hn' : 0 < n')
    (c c' : ι → ℝ) (hc : ∀ i, 0 < c i) (hc' : ∀ i, 0 < c' i)
    (hp : 0 < p) (hε : 0 ≤ ε)
    (frequency : ι → κ → ℝ) (b : ℝ)
    (A A' : ι → EuclideanSpace ℂ κ)
    (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‖ ≤
        ε*(c i/n)^(1/p)*(c i)^μ) :
    1+∑ i, (c i/n)*‖(c i)^(μ-1) • radialShrink (2*ε*c i) (A i)‖^p ≤
…

Mentions: OAI.LipschitzHilbert.massPowerScale, OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.source_balanced_prediction_comparison line 64

Source documentation

In the balanced branch the normalized moving prediction is controlled by the actual shrunken snapshot, with an error proportional to u.

theorem source_balanced_prediction_comparison
    {n n' p μ ε K u : ℝ} (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