OAI/Analysis/LipschitzHilbert/Geometry/FiniteOutputCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite cover of output points permits summing operator bounds. No disjointness or regularity of the choice of a covering index is needed.

  1. theorem OAI.LipschitzHilbert.eLpNorm_le_sum_of_pointwise_choice line 11