OAI/Analysis/LipschitzHilbert/Trees/UnarySegmentEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The segment log estimate with the starred amplitudes actually propagated.

  1. theorem OAI.LipschitzHilbert.unary_propagated_log_drop_bound line 14

    Source documentation

    Retain the exact total drop for the discarded-top contribution.

    theorem unary_propagated_log_drop_bound {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [NormedSpace ℂ E]
    (N : ℕ) (n : ℕ → ℝ) (A U W : ℕ → E) (beta : ℕ → ℝ) (coeff : ℕ → ℂ)
    {a p D ε : ℝ} (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p)
    (hD : 0 ≤ D) (hε : 0 ≤ ε) (hstart : 4 ≤ n 0)
    (hn : ∀ i ≤ N, n 0 - 2 ≤ n i ∧ n i ≤ n 0)
    (hmass : ∀ i < N, n (i + 1) ≤ n i)
    (hcoeff : ∀ i < N, ‖coeff i‖ ≤ 1)
    (hstep : ∀ i < N, A i = coeff i • A (i + 1) + U i + W i)
    (hU : ∀ i ≤ N, ‖∑ j ∈ Finset.Ico i N, unaryPropagator coeff i j • U j‖ ≤ D)
    (hW : ∀ i < N, ‖W i‖ ≤ ε * (n i - n (i + 1)))
    (hbeta : ∀ i < N, 0 < beta i)
…

    Mentions: OAI.LipschitzHilbert.unaryPropagator

  2. theorem OAI.LipschitzHilbert.unary_propagated_log_bound line 48