OAI/Analysis/LipschitzHilbert/Trees/SourcePlanarGramSchur.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Apply the finite Gram-matrix estimate to actual planar Schwartz functions and their product-Lebesgue square integrals.

  1. theorem OAI.LipschitzHilbert.planar_toL2_norm_sq line 13
  2. theorem OAI.LipschitzHilbert.planar_sparse_gram_energy line 22