OAI/Geometry/CubicTorus/Reflection/BVConeSecondaryFlux.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_paired_blowup line 15
  2. lemma OAI.CubicTorus.divergence_radial_smul line 92
  3. theorem OAI.CubicTorus.limit_set_radial_flux line 104
  4. lemma OAI.CubicTorus.hasDerivAt_setIntegral_dilation line 128
  5. lemma OAI.CubicTorus.dilation_tsupport_subset line 173
  6. lemma OAI.CubicTorus.fderiv_dilation_apply line 185
  7. lemma OAI.CubicTorus.dilation_radial_euler line 193
  8. theorem OAI.CubicTorus.radial_flux_dilation_pairing line 242
  9. lemma OAI.CubicTorus.integral_indicator_dilation_local line 280
  10. lemma OAI.CubicTorus.radial_flux_cone_test line 298
  11. theorem OAI.CubicTorus.radial_flux_cone_ae line 316
  12. def OAI.CubicTorus.affineScalarTest line 356
  13. lemma OAI.CubicTorus.affineScalarTest_contDiff line 359
  14. lemma OAI.CubicTorus.affineScalarTest_tsupport line 363
  15. lemma OAI.CubicTorus.fderiv_affineScalarTest line 375
  16. lemma OAI.CubicTorus.affineScalarTest_radial line 384
  17. lemma OAI.CubicTorus.radial_flux_affine_identity line 395
  18. lemma OAI.CubicTorus.local_indicator_pairing_tendsto line 432
  19. lemma OAI.CubicTorus.fderiv_apply_tsupport_subset line 457
  20. lemma OAI.CubicTorus.radial_euler_tsupport_subset line 464
  21. lemma OAI.CubicTorus.indicator_pairing_integrable line 471
  22. theorem OAI.CubicTorus.radial_cone_secondary_derivative_zero line 480
  23. lemma OAI.CubicTorus.hasDerivAt_setIntegral_translation line 534
  24. lemma OAI.CubicTorus.translation_test_tsupport line 562
  25. lemma OAI.CubicTorus.derivative_zero_translation_pairing line 576
  26. theorem OAI.CubicTorus.derivative_zero_translation_ae line 629
  27. theorem OAI.CubicTorus.radial_cone_secondary_line_invariance line 666
  28. lemma OAI.CubicTorus.cone_dilation_pairing line 698
  29. theorem OAI.CubicTorus.cone_radial_euler line 723
  30. lemma OAI.CubicTorus.localL1_triangle line 776
  31. theorem OAI.CubicTorus.actual_tangent_secondary_representation line 788
  32. theorem OAI.CubicTorus.actual_tangent_secondary_limit line 870