OAI/Analysis/LipschitzHilbert/Trees/SourceSimplexLp.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar damped simplex theorem gives a dimension-independent Lp estimate on each bounded exhaustion of the actual packet family.

  1. theorem OAI.LipschitzHilbert.damped_simplex_barycenter_nonneg line 16
  2. theorem OAI.LipschitzHilbert.source_bounded_pairing_bound line 34
  3. theorem OAI.LipschitzHilbert.source_simplex_lp_of_bounded_integrals line 59