OAI/Geometry/CubicTorus/Estimates/SliceJensenWeight.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.sliceJensenCutoff line 12
  2. def OAI.CubicTorus.sliceJensenG line 14
  3. lemma OAI.CubicTorus.sliceJensenCutoff_pos line 18
  4. lemma OAI.CubicTorus.sliceJensenCutoff_sq line 21
  5. lemma OAI.CubicTorus.sliceJensenCutoff_lt_one line 25
  6. lemma OAI.CubicTorus.sqrt_cutoff line 27
  7. lemma OAI.CubicTorus.sliceJensenG_cutoff line 33
  8. theorem OAI.CubicTorus.sliceJensenG_properties line 38
  9. theorem OAI.CubicTorus.slice_jensen_density_inequality line 60
  10. theorem OAI.CubicTorus.circle_jensen_supports_ae line 97
  11. theorem OAI.CubicTorus.circle_conditional_jensen_ae line 146
  12. lemma OAI.CubicTorus.sliceSupport_sum line 175
  13. lemma OAI.CubicTorus.slice_support_endpoint line 194
  14. theorem OAI.CubicTorus.slice_jensen_closed_cone line 224
  15. lemma OAI.CubicTorus.circle_conditional_jensen_closed_ae line 258
  16. lemma OAI.CubicTorus.sliceJensenG_measurable line 282
  17. lemma OAI.CubicTorus.sliceJensenG_mem_Icc line 286
  18. lemma OAI.CubicTorus.circle_jensen_integrable line 298
  19. theorem OAI.CubicTorus.circle_integrated_jensen line 316
  20. def OAI.CubicTorus.axialJensenFlux line 363
  21. lemma OAI.CubicTorus.axialTangentialSpeed_mem_Icc line 367
  22. lemma OAI.CubicTorus.sqrt_one_sub_axialTangentialSpeed_sq line 374
  23. lemma OAI.CubicTorus.axial_flux_smooth_density line 378
  24. theorem OAI.CubicTorus.axial_integrated_jensen line 401
  25. lemma OAI.CubicTorus.circle_unsigned_normal_density line 466
  26. lemma OAI.CubicTorus.normalComponent_integral_sq line 507
  27. lemma OAI.CubicTorus.axialProjection_bound line 524
  28. lemma OAI.CubicTorus.chamber_corner_coordinate_twice line 592
  29. lemma OAI.CubicTorus.chamber_reflected_coordinate line 596
  30. theorem OAI.CubicTorus.isMinimizerAt_chamber_support_positive line 604
  31. lemma OAI.CubicTorus.inner_tangent_projection line 672
  32. lemma OAI.CubicTorus.normal_position_gradient_trace line 678
  33. theorem OAI.CubicTorus.translation_jacobi_position_identity line 706
  34. theorem OAI.CubicTorus.exists_periodic_position_box line 768