UnaryPropagation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact propagation along unary segments

Finite iteration of §10 res:unary-decomposition. The residual coefficient is the actual product of preceding path coefficients. Discarded-top errors are summed against mass drops rather than the number of tops or levels, as required in res:segment-perturbation.

def OAI.LipschitzHilbert.unaryPropagator line 22
theorem OAI.LipschitzHilbert.unaryPropagator_self line 25
theorem OAI.LipschitzHilbert.unaryPropagator_succ_right line 28
theorem OAI.LipschitzHilbert.unaryPropagator_succ_left line 33
theorem OAI.LipschitzHilbert.unaryPropagator_norm_le_one line 38
theorem OAI.LipschitzHilbert.sum_Ico_forward_difference line 49

theorem OAI.LipschitzHilbert.unary_iteration line 59

Source documentation

Iteration retains the exact common product on every residual term.

theorem unary_iteration (coeff : ℕ → ℂ) (A U W : ℕ → E) {start finish : ℕ}
    (h : start ≤ finish)
    (hstep : ∀ i ∈ Finset.Ico start finish, A i = coeff i • A (i + 1) + U i + W i) :
    A start - unaryPropagator coeff start finish • A finish =
      (∑ i ∈ Finset.Ico start finish, unaryPropagator coeff start i • U i) +
      ∑ i ∈ Finset.Ico start finish, unaryPropagator coeff start i • W i := by
…

Mentions: OAI.LipschitzHilbert.unaryPropagator

theorem OAI.LipschitzHilbert.propagated_endpoint_contraction line 77

theorem OAI.LipschitzHilbert.discarded_unary_error_sum line 85

Source documentation

Whole discarded-top errors cost only the total mass drop.

theorem discarded_unary_error_sum (coeff : ℕ → ℂ) (W : ℕ → E) (n : ℕ → ℝ)
    {start finish : ℕ} {ε : ℝ} (h : start ≤ finish)
    (hcoeff : ∀ j ∈ Finset.Ico start finish, ‖coeff j‖ ≤ 1)
    (hW : ∀ j ∈ Finset.Ico start finish, ‖W j‖ ≤ ε * (n j - n (j + 1))) :
    ‖∑ i ∈ Finset.Ico start finish, unaryPropagator coeff start i • W i‖ ≤
      ε * (n start - n finish) := by
…

Mentions: OAI.LipschitzHilbert.unaryPropagator

theorem OAI.LipschitzHilbert.unary_perturbation_bound line 108

Source documentation

The propagated main residual sum and discarded-top error give the amplitude perturbation used by the unary energy telescope.

theorem unary_perturbation_bound (coeff : ℕ → ℂ) (A U W : ℕ → E) (n : ℕ → ℝ)
    {start finish : ℕ} {ε D : ℝ} (h : start ≤ finish)
    (hcoeff : ∀ j ∈ Finset.Ico start finish, ‖coeff j‖ ≤ 1)
    (hstep : ∀ i ∈ Finset.Ico start finish, A i = coeff i • A (i + 1) + U i + W i)
    (hU : ‖∑ i ∈ Finset.Ico start finish, unaryPropagator coeff start i • U i‖ ≤ D)
    (hW : ∀ j ∈ Finset.Ico start finish, ‖W j‖ ≤ ε * (n j - n (j + 1))) :
    ‖A start - unaryPropagator coeff start finish • A finish‖ ≤
      D + ε * (n start - n finish) := by
…

Mentions: OAI.LipschitzHilbert.unaryPropagator