OAI/Analysis/LipschitzHilbert/Phase/GraphPhaseAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted prediction using the explicitly constructed independent-set law.

  1. theorem OAI.LipschitzHilbert.independent_card_le_span line 23
  2. theorem OAI.LipschitzHilbert.graph_weighted_diagonal_prediction_average line 37