OAI/Geometry/CubicTorus/Estimates/PlanarRadialArea.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.square_below_nonnegative_chord line 12
  2. lemma OAI.CubicTorus.firstCorner_chord_endpoint_bound line 20
  3. theorem OAI.CubicTorus.firstCorner_dimensionless_bound line 36
  4. theorem OAI.CubicTorus.firstCorner_scaled_strict_bound line 98
  5. theorem OAI.CubicTorus.firstCorner_endpoint_contradiction line 125
  6. theorem OAI.CubicTorus.isMinimizerAt_boundary_curve_tangent line 242
  7. lemma OAI.CubicTorus.coordinateSectionPoint_hasDerivAt line 285
  8. theorem OAI.CubicTorus.isMinimizerAt_radial_curve_tangent line 291
  9. def OAI.CubicTorus.planarRadialRegion line 316
  10. lemma OAI.CubicTorus.measurableSet_planarRadialRegion line 319
  11. lemma OAI.CubicTorus.mem_planarRadialRegion_polar line 323
  12. lemma OAI.CubicTorus.lintegral_radial_coordinate line 332
  13. theorem OAI.CubicTorus.volume_planarRadialRegion line 345
  14. lemma OAI.CubicTorus.real_volume_planarRadialRegion line 396
  15. theorem OAI.CubicTorus.planar_radial_area_length line 403
  16. lemma OAI.CubicTorus.unit_square_integral_swap line 424
  17. theorem OAI.CubicTorus.periodic_parametric_green line 433
  18. def OAI.CubicTorus.complexDet line 471
  19. def OAI.CubicTorus.complexRealDiv line 473
  20. lemma OAI.CubicTorus.complexDet_continuous line 476
  21. lemma OAI.CubicTorus.complexDet_smul_left line 481
  22. lemma OAI.CubicTorus.complexDet_smul_right line 485
  23. lemma OAI.CubicTorus.complexDet_deriv line 489
  24. lemma OAI.CubicTorus.complexDet_trace_identity line 499
  25. theorem OAI.CubicTorus.complex_green_homotopy line 509
  26. lemma OAI.CubicTorus.polarCoord_symm_unitAngle line 569
  27. lemma OAI.CubicTorus.continuous_polarSymm line 576
  28. lemma OAI.CubicTorus.integral_radial_coordinate line 580
  29. theorem OAI.CubicTorus.integral_planarRadialRegion_polar line 592
  30. lemma OAI.CubicTorus.integral_radial_coordinate_scale line 660
  31. theorem OAI.CubicTorus.integral_planarRadialRegion_homotopy line 676
  32. lemma OAI.CubicTorus.complexRealDiv_continuous line 710
  33. lemma OAI.CubicTorus.complexDet_eq_im line 715
  34. theorem OAI.CubicTorus.green_planarRadialRegion line 718
  35. def OAI.CubicTorus.coordinatePlaneProjection line 749
  36. lemma OAI.CubicTorus.coordinatePlaneProjection_re line 753
  37. lemma OAI.CubicTorus.coordinatePlaneProjection_im line 755
  38. lemma OAI.CubicTorus.coordinatePlaneProjection_inner line 758
  39. lemma OAI.CubicTorus.coordinatePlaneProjection_norm_sq line 765
  40. lemma OAI.CubicTorus.coordinatePlaneProjection_unit line 772
  41. lemma OAI.CubicTorus.complexDet_four_square line 778
  42. lemma OAI.CubicTorus.complexDet_unit_positive line 783
  43. def OAI.CubicTorus.coordinatePlaneField line 803
  44. lemma OAI.CubicTorus.coordinatePlaneField_contDiff line 806
  45. lemma OAI.CubicTorus.coordinatePlaneField_divergence line 811