OAI/Analysis/LipschitzHilbert/Estimates/CubicDualityEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar exponent calculation in the three-halves dual estimate.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.cubic_duality_estimate line 10