OAI/Analysis/LipschitzHilbert/Trees/SourceCentralHolder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The central weight is controlled by the normalized vertex moment and the measure of the common good set. This is the Hölder step in §11.

  1. theorem OAI.LipschitzHilbert.central_weight_factorization line 13
  2. theorem OAI.LipschitzHilbert.central_weight_integral line 21