OAI/Geometry/PrescribedPotential/ChartTransport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Chart Transport.

  1. structure OAI.GlobalElliptic.ChartCutoff line 22
  2. instance OAI.GlobalElliptic.(instance at line 27) line 27
  3. lemma OAI.GlobalElliptic.ChartCutoff.product_smooth line 32
  4. lemma OAI.GlobalElliptic.ChartCutoff.product_compact line 43
  5. def OAI.GlobalElliptic.ChartCutoff.product line 48
  6. lemma OAI.GlobalElliptic.ChartCutoff.product_apply line 51
  7. lemma OAI.GlobalElliptic.ChartCutoff.product_tsupport line 54
  8. def OAI.GlobalElliptic.ChartCutoff.mulOn line 60
  9. lemma OAI.GlobalElliptic.ChartCutoff.deriv_tsupport line 65
  10. def OAI.GlobalElliptic.ChartCutoff.deriv line 78
  11. def OAI.GlobalElliptic.chartTransport line 88
  12. lemma OAI.GlobalElliptic.chartTransport_apply line 97
  13. theorem OAI.GlobalElliptic.chartTransport_l2_bound line 103