OAI/Geometry/IntegralFillings/Currents/WeightedAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.BorelCoefficients.toL1_mul_dist_le line 36
2. lemma OAI.SharpIntegralFillings.BorelCoefficients.tendsto_toL1_mul line 52
3. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_locality_mul line 64
4. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_linearCoord line 106
5. def OAI.SharpIntegralFillings.BorelCoefficients.weightedCurrent line 142
6. lemma OAI.SharpIntegralFillings.BorelCoefficients.weightedCurrent_isMetricCurrent line 145