OAI/Analysis/LipschitzHilbert/Estimates/SquareTailLayer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted layer-cake estimate in the product form produced by the covering inequality. All weights are the actual top areas.

  1. theorem OAI.LipschitzHilbert.weighted_layer_from_square_tail line 12