OAI/Analysis/LipschitzHilbert/Estimates/ColoredPlanarEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing a fixed number of disjoint annular lists costs only that number. In particular the ordinary dyadic synthesis constant is uniform in the number of scales.

  1. theorem OAI.LipschitzHilbert.planar_colored_energy line 16
  2. theorem OAI.LipschitzHilbert.exists_planar_dyadic_energy_constant line 79