OAI/Combinatorics/TriangleRemoval/Coupling/UnitTime.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.unitTime line 17
2. theorem OAI.SharpTerminalLeave.unitTime_nonneg line 19
3. theorem OAI.SharpTerminalLeave.unitTime_le_one line 20
4. theorem OAI.SharpTerminalLeave.unitTime_of_mem line 22
5. theorem OAI.SharpTerminalLeave.continuous_unitTime line 24
6. theorem OAI.SharpTerminalLeave.abs_prod_sub_prod_le_sum line 27
7. def OAI.SharpTerminalLeave.messageCandidates line 62
8. def OAI.SharpTerminalLeave.messageIntegral line 65
9. def OAI.SharpTerminalLeave.cavityOperator line 69
10. def OAI.SharpTerminalLeave.cavityDepth line 73
11. theorem OAI.SharpTerminalLeave.continuous_message_integrand line 78
12. theorem OAI.SharpTerminalLeave.continuous_messageIntegral line 84
13. theorem OAI.SharpTerminalLeave.continuous_cavityOperator line 92
14. theorem OAI.SharpTerminalLeave.continuous_cavityDepth line 99
15. theorem OAI.SharpTerminalLeave.messageIntegral_mem_unit line 106
16. theorem OAI.SharpTerminalLeave.cavityOperator_mem_unit line 123
17. theorem OAI.SharpTerminalLeave.cavityDepth_mem_unit line 136
18. def OAI.SharpTerminalLeave.cavityBranching line 142
19. theorem OAI.SharpTerminalLeave.cavityBranching_nonneg line 145
20. theorem OAI.SharpTerminalLeave.cavityOperator_lipschitz line 149
21. theorem OAI.SharpTerminalLeave.cavityDepth_succ_diff line 224
22. abbrev OAI.SharpTerminalLeave.CavitySpace line 261
23. def OAI.SharpTerminalLeave.cavityDepthBCF line 263
24. theorem OAI.SharpTerminalLeave.cavityDepthBCF_apply line 273
25. theorem OAI.SharpTerminalLeave.cavityDepthBCF_succ_dist line 276
26. theorem OAI.SharpTerminalLeave.cavityDepthBCF_cauchy line 296
27. def OAI.SharpTerminalLeave.cavityLimitBCF line 300
28. theorem OAI.SharpTerminalLeave.tendsto_cavityDepthBCF line 303
29. def OAI.SharpTerminalLeave.cavityLimit line 307
30. theorem OAI.SharpTerminalLeave.continuous_cavityLimit line 310
31. theorem OAI.SharpTerminalLeave.tendsto_cavityDepth line 313
32. theorem OAI.SharpTerminalLeave.cavityLimit_mem_unit line 320
33. theorem OAI.SharpTerminalLeave.cavitySpace_eval_sub_le line 327
34. theorem OAI.SharpTerminalLeave.cavityLimit_product line 332
35. theorem OAI.SharpTerminalLeave.cavityDepth_zero_time line 361
36. theorem OAI.SharpTerminalLeave.cavityLimit_zero_time line 365
37. theorem OAI.SharpTerminalLeave.messageCandidates_omission line 372
38. theorem OAI.SharpTerminalLeave.cavityLimit_omission line 377
39. theorem OAI.SharpTerminalLeave.messageIntegral_le_time line 387
40. theorem OAI.SharpTerminalLeave.cavityLimit_factor_pos line 398
41. theorem OAI.SharpTerminalLeave.cavityLimit_pos line 407
42. theorem OAI.SharpTerminalLeave.messageIntegral_hasDerivAt line 413
43. theorem OAI.SharpTerminalLeave.cavityLimit_hasDerivAt line 426
44. def OAI.SharpTerminalLeave.cavityTime line 459
45. def OAI.SharpTerminalLeave.cavityLog line 461
46. def OAI.SharpTerminalLeave.cavityMessage line 464
47. theorem OAI.SharpTerminalLeave.cavityTime_hasDerivAt line 468
48. theorem OAI.SharpTerminalLeave.cavityTime_zero line 476
49. theorem OAI.SharpTerminalLeave.cavityLog_zero line 479
50. theorem OAI.SharpTerminalLeave.cavityLog_exp line 482
51. theorem OAI.SharpTerminalLeave.cavityLog_parent line 488
52. theorem OAI.SharpTerminalLeave.cavityLog_hasDerivAt line 496
53. theorem OAI.SharpTerminalLeave.cavityMessage_hasDerivAt line 511
54. theorem OAI.SharpTerminalLeave.triangle_children line 522
55. theorem OAI.SharpTerminalLeave.cavity_triangle_summand line 534
56. theorem OAI.SharpTerminalLeave.cavity_triangle_message_summand line 558
57. theorem OAI.SharpTerminalLeave.continuous_cavityTime line 580
58. theorem OAI.SharpTerminalLeave.cavityTime_mono line 584
59. theorem OAI.SharpTerminalLeave.cavityTime_pos line 590
60. theorem OAI.SharpTerminalLeave.continuous_cavityMessage line 594
61. theorem OAI.SharpTerminalLeave.cavityMessage_zero line 599
62. theorem OAI.SharpTerminalLeave.cavityMessage_nonneg line 603
63. theorem OAI.SharpTerminalLeave.continuousOn_cavityLog line 608