DiagonalFamilyContinuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform component estimates give norm-continuous spatial families

theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_sub_eq line 16

theorem OAI.CoarseAssembly.DiscreteRoe.diagonalFamily_sub_norm_le line 30

Source documentation

The bound does not depend on the number or sizes of the components.

theorem diagonalFamily_sub_norm_le (A B : ∀ i, Operator (V i) H)
    (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hA : ∀ i, ‖A i‖ ≤ C) (hB : ∀ i, ‖B i‖ ≤ D)
    (δ : ℝ) (hδ : 0 ≤ δ) (hAB : ∀ i, ‖A i - B i‖ ≤ δ) :
    ‖diagonalFamily A C hC hA - diagonalFamily B D hD hB‖ ≤ δ := by
…

Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator, OAI.CoarseAssembly.DiscreteRoe.diagonalFamily

theorem OAI.CoarseAssembly.DiscreteRoe.continuous_diagonalFamily line 38