SourceDominantPrediction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual dominant-path coordinates for the source prediction. The path amplitude stays unshrunk; only the complementary children are shrunk.

theorem OAI.LipschitzHilbert.diagonalModulation_inverse line 22

Source documentation

Removing the snapshot path carrier is an exact isometry.

theorem diagonalModulation_inverse (f : κ → ℝ) (v : EuclideanSpace ℂ κ) (b : ℝ) :
    diagonalModulation (fun k => -f k) (diagonalModulation f v b) b = v := by
…

theorem OAI.LipschitzHilbert.source_path_prediction_identity line 32

Source documentation

Exact dominant coordinates for a finite normalized prediction. The rotation may be the inverse of the actual path carrier.

theorem source_path_prediction_identity
    (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
    (i₀ : ι) (U : EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ)
    {p μ : ℝ} (hp : 0 < p) (hl : 0 < l i₀) (hlam : lam i₀ ≠ 0) :
    let Y := (l i₀)^(1/p) • U (X i₀)
…

theorem OAI.LipschitzHilbert.source_path_vector_motion line 84

Source documentation

The scaled source amplitude is the actual path vector, including its child fraction. No lower bound on that fraction is needed.

theorem source_path_vector_motion {n n' c c' p μ ε K : ℝ}
    (hn : 0 < n) (hn' : 0 < n') (hc : 0 < c) (hc' : 0 < c')
    (hcn : c ≤ n) (hp : 0 < p) (hμ : 0 ≤ μ) (hε : 0 ≤ ε)
    (hK : n^μ ≤ K) (f : κ → ℝ) (b : ℝ) (A A' : EuclideanSpace ℂ κ)
    (hscaled : ‖massPowerScale n' c' (-(1/p)) (μ-1+1/p) • A'-
      diagonalModulation f (massPowerScale n c (-(1/p)) (μ-1+1/p) • A) b‖ ≤
      ε*(c/n)^(1/p)*c^μ) :
    ‖(c'/n')^(1/p) • diagonalModulation (fun k => -f k) (c'^(μ-1) • A') b-
      (c/n)^(1/p) • (c^(μ-1) • A)‖ ≤ ε*K := by
…

Mentions: OAI.LipschitzHilbert.massPowerScale

theorem OAI.LipschitzHilbert.source_path_vector_size line 131

Source documentation

Snapshot path size and its moved counterpart use the same parent mass scale as the off-path coefficient budget.

theorem source_path_vector_size {n c p μ C K : ℝ}
    (hn : 0 < n) (hc : 0 < c) (hcn : c ≤ n) (hp : 0 < p)
    (hμ : 0 ≤ μ) (hC : 0 ≤ C) (hsize : C*n^μ ≤ K)
    (A : EuclideanSpace ℂ κ) (hA : ‖A‖ ≤ C*c) :
    ‖(c/n)^(1/p) • (c^(μ-1) • A)‖ ≤ K := by
…

theorem OAI.LipschitzHilbert.source_off_path_residual_order line 153

Source documentation

The one-sided source shrink bounds add over precisely the complementary children; no comparison of the full path denominator is assumed.

theorem source_off_path_residual_order
    {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 ≤ ε) (f : ι → κ → ℝ) (b : ℝ)
    (A A' : ι → EuclideanSpace ℂ κ)
    (hscaled : ∀ i,
      ‖massPowerScale n' (c' i) (-(1/p)) (μ-1+1/p) • A' i-
        diagonalModulation (f i)
          (massPowerScale n (c i) (-(1/p)) (μ-1+1/p) • A i) b‖ ≤
        ε*(c i/n)^(1/p)*(c i)^μ) :
    (∑ i, (c i/n)*‖(c i)^(μ-1) • radialShrink (2*ε*c i) (A i)‖^p) ≤
      ∑ i, (c' i/n')*‖(c' i)^(μ-1) • A' i‖^p := by
…

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

theorem OAI.LipschitzHilbert.source_numerator_term_bound line 168

theorem OAI.LipschitzHilbert.source_off_path_coordinate_size line 181

Source documentation

The removed path phase and carrier do not change the off-path size.

theorem source_off_path_coordinate_size {n μ ε K C u : ℝ}
    (hn : 0 < n) (hε : 0 ≤ ε) (hK : 0 ≤ K) (hC : 0 ≤ C) (hsize : C*n^μ ≤ K)
    (c : ι → ℝ) (hc : ∀ i, 0 < c i) (hmass : ∑ i, c i/n ≤ u)
    (f : ι → κ → ℝ) (b : ℝ) (U : EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ)
    (A : ι → EuclideanSpace ℂ κ) (lam : ι → ℂ)
    (hlam : ∀ i, ‖lam i‖ ≤ 1) (hA : ∀ i, ‖A i‖ ≤ C*c i)
    (pathLam : ℂ) (hpath : pathLam ≠ 0) :
    ‖(scalarPhase pathLam)⁻¹ • U (∑ i, ((n^(μ-1):ℝ):ℂ) •
      (lam i • diagonalModulation (f i) (radialShrink (2*ε*c i) (A i)) b))‖ ≤ K*u := by
…

Mentions: OAI.LipschitzHilbert.scalarPhase, OAI.LipschitzHilbert.radialShrink

theorem OAI.LipschitzHilbert.source_off_path_coordinate_motion line 207

Source documentation

Simultaneously rotate all complementary children into the path frame. The coefficient of the error still vanishes with their total mass.

theorem source_off_path_coordinate_motion
    {n n' μ ε K C q u : ℝ} (hn : 0 < n) (_hn' : 0 < n')
    (hε : 0 ≤ ε) (hK : 0 ≤ K) (_hC : 0 ≤ C) (hpower : n^μ ≤ K)
    (hsize : C*n^μ ≤ K) (hq0 : 0 ≤ q) (hq1 : q < 1)
    (c : ι → ℝ) (hc : ∀ i, 0 < c i) (hmass : ∑ i, c i/n ≤ u)
    (f : ι → κ → ℝ) (b : ℝ) (U : EuclideanSpace ℂ κ →ₗᵢ[ℂ] EuclideanSpace ℂ κ)
    (A A' : ι → EuclideanSpace ℂ κ) (lam lam' : ι → ℂ)
    (hlam : ∀ i, ‖lam i‖ ≤ 1) (hA : ∀ i, ‖A i‖ ≤ C*c i)
    (hmove : ∀ i,
      ‖((n'^(μ-1):ℝ):ℂ) • (lam' i • A' i)-
        ((n^(μ-1):ℝ):ℂ) • (lam i • diagonalModulation (f i) (A i) b)‖ ≤
        ε*K*(c i/n))
…

theorem OAI.LipschitzHilbert.source_dominant_coordinate_control line 256

Source documentation

The original child-mass error bounds imply all dominant-path errors at once, with no assumed residual ordering. The scalar-coefficient bounds are supplied by the complementary-mass theorem.

theorem source_dominant_coordinate_control
    {n n' p μ ε K C q u : ℝ} (hn : 0 < n) (hn' : 0 < n')
    (hp : 0 < p) (hμ : 0 ≤ μ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1)
    (hK : 0 ≤ K) (hC : 0 ≤ C) (hpower : n^μ ≤ K) (hsize : C*n^μ ≤ K)
    (c c' : ι → ℝ) (hc : ∀ i, 0 < c i) (hc' : ∀ i, 0 < c' i)
    (i₀ : ι) (hcn : c i₀ ≤ n)
    (hmass : ∑ i : RemainderIndex i₀, c i/n ≤ u)
    (f : ι → κ → ℝ) (b : ℝ)
    (A A' : ι → EuclideanSpace ℂ κ) (lam lam' : ι → ℂ)
    (hlam : ∀ i, ‖lam i‖ ≤ 1) (hpath : lam i₀ ≠ 0)
    (hq0 : 0 ≤ q) (hq1 : q < 1) (hqε : q ≤ ε)
    (hphase : ‖lam' i₀-lam i₀‖ ≤ q*‖lam i₀‖)
…