ResidualBlocks.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Square summation of disjoint residual blocks

The finite deterministic estimates in §10 res:block-square: error envelopes are summed in ℓ¹, main envelopes in ℓ², and each block contains only a bounded number of lengths. Multiplicities of packets at one length are already included in the corresponding envelope.

theorem OAI.LipschitzHilbert.sum_disjoint_blocks_le line 23
theorem OAI.LipschitzHilbert.error_blocks_square_sum_le line 34
theorem OAI.LipschitzHilbert.main_blocks_square_sum_le line 46

theorem OAI.LipschitzHilbert.residual_blocks_square_sum_le line 62

Source documentation

A residual block is controlled by its error and main envelopes and a final-block remainder. Their full square sum has no depth factor.

theorem residual_blocks_square_sum_le {E : Type*} [NormedAddCommGroup E]
    (I : ι → Finset κ) (hI : Pairwise (fun i j => Disjoint (I i) (I j)))
    (e a : κ → ℝ) (he : ∀ k, 0 ≤ e k) (ha : ∀ k, 0 ≤ a k)
    (B : ι → E) (r : ι → ℝ) (hr : ∀ i, 0 ≤ r i)
    {C L R : ℝ} (_hC : 0 ≤ C) (hL : 0 ≤ L) (hR : 0 ≤ R)
    (hcard : ∀ i, ((I i).card : ℝ) ≤ L) (hremainder : ∑ i, r i ≤ R)
    (hbound : ∀ i, ‖B i‖ ≤ C * ((∑ k ∈ I i, e k) + ∑ k ∈ I i, a k) + r i) :
    (∑ i, ‖B i‖ ^ 2) ≤
      3 * C ^ 2 * ((∑ k, e k) ^ 2 + L * ∑ k, (a k) ^ 2) + 3 * R ^ 2 := by
…