OAI/Geometry/IsometricImmersion/Energy/MultiplierAbsorption.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Weighted.normalized_T_lower_bound line 12
2. theorem OAI.SmoothLocal.Weighted.quadratic_cross_absorption line 25
3. theorem OAI.SmoothLocal.Weighted.cross_loss_bound line 37
4. theorem OAI.SmoothLocal.Weighted.positive_strip_weight_bound line 66
5. theorem OAI.SmoothLocal.Weighted.exists_positive_strip_scale line 84