OAI/Analysis/LipschitzHilbert/Estimates/L2SpatialPartition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Squaring and summing local L2 estimates over a measurable partition, with a finite overlap bound for the enlarged input sets.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.l2Indicator_norm_sq line 16
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.l2Indicator_finite_overlap line 25
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.l2Indicator_partition_bound line 60