OAI/Geometry/NodalSets/Elliptic/RealWeightedTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Yau.real_pairing_compact line 11
2. lemma OAI.Yau.real_pairing_mul line 17
3. def OAI.Yau.weightedSkewTransport line 25
4. lemma OAI.Yau.weightedSkewTransport_smooth line 29
5. lemma OAI.Yau.weightedSkewTransport_compact line 35
6. lemma OAI.Yau.compact_weighted_product_integrable line 40
7. theorem OAI.Yau.weighted_transport_green line 45
8. lemma OAI.Yau.weightedSkewTransport_mul line 81
9. theorem OAI.Yau.weighted_transport_multiplier line 90