OAI/Geometry/IsometricImmersion/Energy/MultiplierDivergence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Weighted.multiplierOperator line 12
2. def OAI.SmoothLocal.Weighted.multiplierTest line 16
3. def OAI.SmoothLocal.Weighted.multiplierFluxT line 19
4. def OAI.SmoothLocal.Weighted.multiplierFluxS line 24
5. theorem OAI.SmoothLocal.Weighted.multiplierFluxT_partial_t line 31
6. theorem OAI.SmoothLocal.Weighted.multiplierFluxS_partial_s line 56
7. theorem OAI.SmoothLocal.Weighted.multiplier_divergence_identity line 83
8. theorem OAI.SmoothLocal.Weighted.directed_test_factor line 105
9. theorem OAI.SmoothLocal.Weighted.directed_flux_factor line 113
10. theorem OAI.SmoothLocal.Weighted.directed_flux_edge_zero line 127