OAI/Geometry/CubicTorus/Profiles/PlanarProfile.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Shape.shape_nonneg line 18
2. lemma OAI.ReusedScalar205.CubicTorus.Shape.shape_le_one line 22
3. lemma OAI.ReusedScalar205.CubicTorus.Shape.shape_max line 26
4. lemma OAI.ReusedScalar205.CubicTorus.Shape.continuous_shape line 36
5. lemma OAI.ReusedScalar205.CubicTorus.Shape.integral_eq_split line 40
6. lemma OAI.ReusedScalar205.CubicTorus.Shape.moment_eq line 69
7. lemma OAI.ReusedScalar205.CubicTorus.Shape.firstMoment_eq line 75
8. lemma OAI.ReusedScalar205.CubicTorus.Shape.moment_pos line 107
9. lemma OAI.ReusedScalar205.CubicTorus.Shape.meanQ_eq line 114
10. lemma OAI.ReusedScalar205.CubicTorus.Shape.meanQ_mem line 123
11. theorem OAI.ReusedScalar205.CubicTorus.Shape.moment_bounds line 134
12. lemma OAI.ReusedScalar205.CubicTorus.Shape.affine_shape_integral line 151
13. lemma OAI.ReusedScalar205.CubicTorus.Shape.cubic_shape_lower line 164
14. lemma OAI.ReusedScalar205.CubicTorus.Shape.cubic_shape_lower_dm line 195
15. lemma OAI.ReusedScalar205.CubicTorus.Shape.p₂_pos line 209
16. lemma OAI.ReusedScalar205.CubicTorus.Shape.coefficient_lower line 213
17. theorem OAI.ReusedScalar205.CubicTorus.Shape.uniform_coefficient line 233
18. lemma OAI.ReusedScalar205.CubicTorus.NestingGain.continuousOn_weight line 282
19. lemma OAI.ReusedScalar205.CubicTorus.NestingGain.nesting_parameters line 287
20. lemma OAI.ReusedScalar205.CubicTorus.NestingGain.pointwise_uniform_gain line 310
21. theorem OAI.ReusedScalar205.CubicTorus.NestingGain.integrated_uniform_gain line 332
22. def OAI.ReusedScalar205.CubicTorus.Scalar.planarProfile line 383
23. def OAI.ReusedScalar205.CubicTorus.Scalar.baseline line 386
24. def OAI.ReusedScalar205.CubicTorus.Scalar.P line 389
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Q line 391
26. def OAI.ReusedScalar205.CubicTorus.Scalar.C₀ line 393
27. def OAI.ReusedScalar205.CubicTorus.Scalar.cappedEnergy line 395
28. def OAI.ReusedScalar205.CubicTorus.Scalar.cappedInf line 398
29. def OAI.ReusedScalar205.CubicTorus.Scalar.gain line 401
30. def OAI.ReusedScalar205.CubicTorus.Scalar.critical line 403
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.critical_spec line 406
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.cubic_energy_min line 421
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.cappedEnergy_nonneg line 437
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.cappedInf_formula line 442
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_parameters_pos line 496
36. theorem OAI.ReusedScalar205.CubicTorus.Scalar.gain_formula line 523
37. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_nonneg line 530
38. def OAI.ReusedScalar205.CubicTorus.Scalar.rho line 544
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.nonneg_quadratic_sublevel line 547
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_spec line 561
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_pos line 588
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_zero line 597
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.monotoneOn_rho line 599
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_inverse_sublevel line 608
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_at_inverse line 621
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.antitoneOn_t line 631
47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.monotoneOn_ht line 639
48. def OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument line 655
49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.div_min_positive line 657
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument_eq line 663
51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument_nonneg line 685
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument_continuousOn line 689
53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument_sublevel line 703
54. theorem OAI.ReusedScalar205.CubicTorus.Scalar.fluxArgument_sublevel_set line 717
55. def OAI.ReusedScalar205.CubicTorus.Scalar.density line 741
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.density_nonneg line 743
57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_density line 749
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_neg_rawWeight line 756
59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_density_tail line 762
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_density line 773
61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.weight_layer_cake line 778
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.measurable_fluxArgument line 806
63. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_flux_sublevel line 810
64. theorem OAI.ReusedScalar205.CubicTorus.Scalar.baseline_layer_cake line 827
65. def OAI.ReusedScalar205.CubicTorus.Scalar.rhoRoot line 874
66. def OAI.ReusedScalar205.CubicTorus.Scalar.rhoDen line 875
67. def OAI.ReusedScalar205.CubicTorus.Scalar.rhoSlope line 876
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rhoRoot_pos line 878
69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rhoRoot_sq line 879
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rhoDen_pos line 881