OAI/Geometry/IntegralFillings/Currents/BorelAction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpIntegralFillings.BorelCoefficients.coefficientLinear line 34
  2. lemma OAI.SharpIntegralFillings.BorelCoefficients.coefficientLinear_bound line 45
  3. def OAI.SharpIntegralFillings.BorelCoefficients.l1Action line 53
  4. lemma OAI.SharpIntegralFillings.BorelCoefficients.l1Action_eq line 57
  5. lemma OAI.SharpIntegralFillings.BorelCoefficients.l1Action_bound line 65
  6. def OAI.SharpIntegralFillings.BorelCoefficients.borelAction line 72
  7. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_of_integrable line 77
  8. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_eq line 83
  9. lemma OAI.SharpIntegralFillings.BorelCoefficients.norm_toL1_integral_abs line 95
  10. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_bound line 102
  11. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_add line 109
  12. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_smul line 119
  13. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_congr_ae line 128
  14. lemma OAI.SharpIntegralFillings.BorelCoefficients.l1Action_lipschitz line 140
  15. lemma OAI.SharpIntegralFillings.BorelCoefficients.borelAction_sequentialContinuity line 149