OAI/Geometry/CubicTorus/Profiles/SharpSectionWeight.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.circle_ae_of_upper_half line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_planar_profile_circle line 39
  3. theorem OAI.CubicTorus.isMinimizerAt_nesting_improved_profile_circle line 71
  4. def OAI.CubicTorus.sharpSectionWeight line 126
  5. lemma OAI.CubicTorus.unitPlanarProfile_pos line 129
  6. lemma OAI.CubicTorus.sharpSectionWeight_measurable line 138
  7. lemma OAI.CubicTorus.sharpSectionWeight_nonneg line 144
  8. lemma OAI.CubicTorus.sharpSectionWeight_zero line 151
  9. lemma OAI.CubicTorus.sharpSectionWeight_one line 154
  10. lemma OAI.CubicTorus.sharpSectionWeight_le line 157
  11. def OAI.CubicTorus.improvedSectionWeight line 188
  12. lemma OAI.CubicTorus.improvedSectionWeight_measurable line 193
  13. lemma OAI.CubicTorus.improvedSectionWeight_mem line 199
  14. lemma OAI.CubicTorus.improvedSectionWeight_le_density line 217
  15. lemma OAI.CubicTorus.rational_quadratic_discriminant line 252
  16. theorem OAI.CubicTorus.axial_moment_bounds line 262
  17. lemma OAI.CubicTorus.Nesting.moment_weight_bound_pos line 307
  18. lemma OAI.CubicTorus.Nesting.moment_weight_bound line 348
  19. lemma OAI.CubicTorus.Nesting.continuousOn_weight line 365
  20. lemma OAI.CubicTorus.normalized_real_pair line 382
  21. lemma OAI.CubicTorus.real_pair_dot_le_one line 405
  22. lemma OAI.CubicTorus.integrable_mul_unit line 412
  23. theorem OAI.CubicTorus.axial_density_coarea_bound line 421
  24. lemma OAI.CubicTorus.measurable_nesting_weight_comp line 482
  25. lemma OAI.CubicTorus.axialAreaDensity_integral line 491
  26. lemma OAI.CubicTorus.axialSecondDensity_integral line 498
  27. lemma OAI.CubicTorus.axial_weighted_normal_integrable line 509
  28. theorem OAI.CubicTorus.axial_integrated_flux line 527
  29. lemma OAI.CubicTorus.one_lipschitz_comp_ac line 555
  30. lemma OAI.CubicTorus.bounded_primitive_lipschitz line 566
  31. theorem OAI.CubicTorus.circle_ac_weighted_oscillation line 578
  32. lemma OAI.CubicTorus.axial_integrated_flux_actual line 625
  33. theorem OAI.CubicTorus.isMinimizerAt_weighted_area_bound line 642
  34. lemma OAI.CubicTorus.real_measure_le_of_unit_continuous line 706
  35. theorem OAI.CubicTorus.circle_ac_measurable_weight_integrable line 765
  36. theorem OAI.CubicTorus.circle_ac_measurable_weight line 813