OAI/Geometry/TamingCompatibility/Hodge/HodgeWeightedAdjoint.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integrable_inner_compact_left line 25
2. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integral_inner_fderiv line 34
3. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.weightedAdjoint_pairing line 47
4. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integral_weightedAdjoint line 61
5. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.exists_smooth_extension_compact line 125
6. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integrable_inner_compact_local line 148
7. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integral_inner_fderiv_on line 164
8. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integral_weightedAdjoint_on line 181