OAI/Analysis/LipschitzHilbert/Fourier/ConvolutionThird.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Real interpolation at exponent three for bounded measurable inputs. The proof integrates the two amplitude-dependent Markov bounds.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.highLayerEnergy_measurable line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lowLayerEnergy_measurable line 19
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.convolution_third_lintegral line 26
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.memLp_two_four_integrable_cube line 67
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.convolution_third_bound line 77