OAI/MeasureTheory/Falconer/Estimates/FiniteHolder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The equal-exponent finite Hölder inequality for coordinate deletion

This is the finite sum inequality needed in the induction proving the exact lattice Loomis–Whitney input. It follows from weighted arithmetic–geometric mean after normalizing each row by its actual sum.

  1. theorem OAI.Falconer.finite_holder_equal line 16