OAI/Combinatorics/HoneycombCorridor/LateralLength.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.eventVisitMass line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.sourceExit_visit_sum line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.lateralLengthMass_fubini line 28
  4. theorem OAI.PolynomialVacuumBridge.Corridor.eventVisitMass_le_lateral line 41
  5. theorem OAI.PolynomialVacuumBridge.Corridor.eventVisitMass_exp line 57
  6. theorem OAI.PolynomialVacuumBridge.Corridor.lateralLengthMass_exp line 87
  7. theorem OAI.PolynomialVacuumBridge.Corridor.finite_lateral_tail line 111