OAI/Combinatorics/HoneycombCorridor/CorridorTransfer.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeMean_eq_tsum line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.confinedMean_eq_tsum line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.Subpower.div line 19
  4. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeMean_subpower_of_masses line 28
  5. theorem OAI.PolynomialVacuumBridge.Corridor.confinedMean_subpower_of_masses line 36
  6. def OAI.PolynomialVacuumBridge.Corridor.BridgeReachesDistance line 44
  7. def OAI.PolynomialVacuumBridge.Corridor.bridgeTailMass line 47
  8. def OAI.PolynomialVacuumBridge.Corridor.bridgeTailLengthMass line 51
  9. theorem OAI.PolynomialVacuumBridge.Corridor.reachesDistance_bridgeWord line 56
  10. theorem OAI.PolynomialVacuumBridge.Corridor.weight_nonneg line 61
  11. theorem OAI.PolynomialVacuumBridge.Corridor.firstLengthWeight_nonneg line 64
  12. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeTailMass_le line 68
  13. theorem OAI.PolynomialVacuumBridge.Corridor.bridgeTailLengthMass_le line 82
  14. theorem OAI.PolynomialVacuumBridge.Corridor.not_InLogCorridor_reaches line 99
  15. theorem OAI.PolynomialVacuumBridge.Corridor.logCorridor_loss_le line 110
  16. theorem OAI.PolynomialVacuumBridge.Corridor.logCorridor_mass_error line 137
  17. theorem OAI.PolynomialVacuumBridge.Corridor.logCorridor_length_error line 145
  18. theorem OAI.PolynomialVacuumBridge.Corridor.tendsto_rpow_mul_logGaussian line 154
  19. theorem OAI.PolynomialVacuumBridge.Corridor.tendsto_rpow_mul_logTailExp line 174
  20. theorem OAI.PolynomialVacuumBridge.Corridor.logCorridor_mass_error_superpolynomial line 193
  21. theorem OAI.PolynomialVacuumBridge.Corridor.logCorridor_length_error_superpolynomial line 208
  22. theorem OAI.PolynomialVacuumBridge.Corridor.Subpower.eventually_rpow_le line 235
  23. theorem OAI.PolynomialVacuumBridge.Corridor.Subpower.error_div_tendsto_zero line 246
  24. theorem OAI.PolynomialVacuumBridge.Corridor.Subpower.of_ratio line 264
  25. theorem OAI.PolynomialVacuumBridge.Corridor.subpower_iff_of_superpolynomial_error line 283
  26. theorem OAI.PolynomialVacuumBridge.Corridor.confinedMass_subpower_iff line 308
  27. theorem OAI.PolynomialVacuumBridge.Corridor.confinedLengthMass_subpower_iff line 316