OAI/Analysis/LipschitzHilbert/Estimates/ReferenceSynthesisL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The L1 synthesis estimate that supplies the dual local coefficient budget. Reference length need not be a dyadic scale.

  1. theorem OAI.LipschitzHilbert.ReferencePacketFamily.threshold_lintegral line 17