OAI/Combinatorics/EditApproximation/Geometry/UnifiedPhysicalTable.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The cache's unified index uses warmup indices through T and then refinement indices T+t. Refinement zero is exactly warmup T, including terminal physical nodes and short source intervals.

  1. theorem OAI.EditApproximation.physicalLocalWarmup_terminal line 11
  2. theorem OAI.EditApproximation.physicalLocalRefinement_zero line 27
  3. def OAI.EditApproximation.unifiedPhysicalValue line 51
  4. theorem OAI.EditApproximation.unifiedPhysicalValue_warmup line 55
  5. theorem OAI.EditApproximation.unifiedPhysicalValue_refinement line 60