OAI/Analysis/CircleDomains/Selection/RecursiveReductionBase.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The compact recursive law in the original base presentation. The fallback point and the equivalent restricted homeomorphism have no effect on physical costs.

  1. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.base_finite_length line 23
  2. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.base_occupation line 32
  3. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.base_hit_square_summable line 40
  4. def OAI.CircleDomainRigidity.CompactRecursiveReduction.baseHitWeight line 46
  5. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.base_small line 50
  6. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.baseHitWeight_square_finite line 58
  7. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.baseHitWeight_le line 63
  8. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.avoids_domain line 67
  9. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.physical_start_distance_base line 90