OAI/Analysis/LipschitzHilbert/Fourier/VerticalNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Dimension-independent vertical neighborhood control from the actual function and its vertical derivative. The moment application only needs this fixed interval Sobolev estimate.

  1. theorem OAI.LipschitzHilbert.interval_pointwise_square line 14
  2. theorem OAI.LipschitzHilbert.vertical_neighborhood_square line 49