OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedPairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cauchy--Schwarz pairs the packed short envelopes with the actual weighted long-tree maximum. All weights are explicit functions.

  1. theorem OAI.LipschitzHilbert.reciprocal_weighted_pairing_sq line 11
  2. theorem OAI.LipschitzHilbert.short_long_weighted_pairing_sq line 53