OAI/Analysis/LipschitzHilbert/Geometry/SourceTransverseTreeMaximal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transverse polynomial energy for the actual interval maximum, including finite label slots, from the published scalar Lépingle input.

  1. theorem OAI.LipschitzHilbert.interval_max_le_variation line 12

    Also declared: OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedTreeMaximal.lean:31 (same declaration text).

  2. theorem OAI.LipschitzHilbert.interval_max_sum_le line 18

    Also declared: OAI/Analysis/LipschitzHilbert/Trees/SourceWeightedTreeMaximal.lean:48 (same declaration text).

  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.exists_transverse_physical_tree_maximal line 37
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_transverse_labeled_tree_maximal line 81