OAI/Analysis/LipschitzHilbert/Estimates/ReferenceCarleson.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The local Carleson budget for the actual main analyzing coefficients in a reference box, conditional only on scalar Lépingle.
- theorem
OAI.LipschitzHilbert.ReferencePacketFamily.mainCoefficient_carlesonline 18