OAI/Geometry/PrescribedPotential/LocalizedPullback.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Localized Pullback.

  1. lemma OAI.GlobalElliptic.map_restrict_le_of_jacobian_lower line 19
  2. theorem OAI.GlobalElliptic.exists_map_restrict_bound line 48
  3. lemma OAI.GlobalElliptic.chart_fderiv_det_ne_zero line 75
  4. theorem OAI.GlobalElliptic.chart_map_restrict_bound line 96
  5. def OAI.MeasureTheory.Lp.extendZeroFun line 116
  6. lemma OAI.MeasureTheory.Lp.coeFn_extendZeroFun line 121
  7. lemma OAI.MeasureTheory.Lp.extendZeroFun_add line 125
  8. lemma OAI.MeasureTheory.Lp.extendZeroFun_smul line 137
  9. lemma OAI.MeasureTheory.Lp.norm_extendZeroFun line 149
  10. def OAI.MeasureTheory.Lp.extendZero line 154
  11. lemma OAI.MeasureTheory.Lp.coeFn_extendZero line 161
  12. def OAI.MeasureTheory.Lp.pullbackBounded line 165
  13. lemma OAI.MeasureTheory.Lp.coeFn_pullbackBounded line 170
  14. lemma OAI.MeasureTheory.Lp.pullbackBounded_norm_le line 177