OAI/Analysis/LipschitzHilbert/Estimates/BinaryDensityBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite binary subdivision used for the far-group mass estimate. A bad child is bounded using its good parent; good children are subdivided until the terminal scale.

  1. def OAI.LipschitzHilbert.binaryChildCenter line 12
  2. theorem OAI.LipschitzHilbert.binary_density_bound line 15