OAI/Analysis/LipschitzHilbert/Trees/SourceCentralHolderAE.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The central Hölder estimate needs the mass cap only almost everywhere. In the application the measure is restricted to the constructed common good set.

  1. theorem OAI.LipschitzHilbert.central_weight_integral_ae line 14