OAI/Geometry/PolarProducts/StripEmbedding.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolarStrips.phase line 42
2. theorem OAI.PolarStrips.contDiffAt_phase line 45
3. theorem OAI.PolarStrips.momentum_monotonic line 55
4. theorem OAI.PolarStrips.injOn_phase line 79
5. theorem OAI.ComplexPotential.ddc_holomorphic_norm_sq line 101
6. def OAI.ComplexPotential.phaseForm line 119
7. theorem OAI.ComplexPotential.standardTensor_parts line 122
8. theorem OAI.ComplexPotential.standardTensor_coordinates line 132
9. theorem OAI.ComplexPotential.scalar_wedge_mul line 140
10. theorem OAI.PolarStrips.fderiv_tuple_apply line 156
11. theorem OAI.PolarStrips.norm_coefficient line 170
12. theorem OAI.PolarStrips.fderiv_phase_apply line 178
13. theorem OAI.PolarStrips.phase_form_formula line 200
14. theorem OAI.PolarStrips.phase_pullback line 229
15. def OAI.ConvexPolar.polar line 261
16. theorem OAI.ConvexPolar.polar_antitone line 263
17. theorem OAI.ConvexPolar.mem_interior_polar_of_bound line 266
18. def OAI.ConvexPolar.stripBody line 287
19. theorem OAI.ConvexPolar.mem_interior_stripBody line 291
20. theorem OAI.ConvexPolar.zero_mem_interior_stripBody line 303
21. theorem OAI.ConvexPolar.isCompact_stripBody line 309