OAI/Analysis/Conductivity/Sobolev/NonlinearLp.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.unifIntegrable_of_norm_domination line 12
  2. lemma OAI.ScalarConductivity.continuous_comp_tendstoInMeasure line 26
  3. lemma OAI.ScalarConductivity.nonlinear_memLp line 40
  4. def OAI.ScalarConductivity.nonlinearLp line 51
  5. lemma OAI.ScalarConductivity.nonlinearLp_coe_ae line 59
  6. theorem OAI.ScalarConductivity.nonlinearLp_continuous line 68
  7. instance OAI.ScalarConductivity.ballMeasure_finite line 101
  8. lemma OAI.ScalarConductivity.smoothJets_zero line 104
  9. lemma OAI.ScalarConductivity.smoothJets_add line 108
  10. lemma OAI.ScalarConductivity.smoothJets_smul line 121
  11. lemma OAI.ScalarConductivity.span_smoothJets line 132
  12. lemma OAI.ScalarConductivity.H1Space_eq_closure line 140
  13. lemma OAI.ScalarConductivity.zeroTraceAmbient_eq_closure line 144
  14. lemma OAI.ScalarConductivity.nonlinear_closure_preservation line 148
  15. def OAI.ScalarConductivity.jetSuperposition line 154
  16. lemma OAI.ScalarConductivity.jetSuperposition_continuous line 157
  17. def OAI.ScalarConductivity.jetSuperpositionBound line 162
  18. lemma OAI.ScalarConductivity.jetSuperpositionBound_nonneg line 165
  19. lemma OAI.ScalarConductivity.jetSuperposition_bound line 169
  20. lemma OAI.ScalarConductivity.gradient_comp_scalar line 189
  21. lemma OAI.ScalarConductivity.smoothJet_comp line 196