OAI/Geometry/PrescribedPotential/GlobalConjugation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Global Conjugation.

  1. def OAI.GlobalElliptic.ChartCutoff.conjugate line 22
  2. lemma OAI.GlobalElliptic.ChartCutoff.conjugate_apply line 33
  3. def OAI.GlobalElliptic.Smooth.conjugate line 38
  4. lemma OAI.GlobalElliptic.Smooth.conjugate_apply line 42
  5. def OAI.GlobalElliptic.Smooth.realify line 44
  6. lemma OAI.GlobalElliptic.Smooth.realify_apply line 45
  7. lemma OAI.GlobalElliptic.Smooth.realify_real line 49
  8. lemma OAI.GlobalElliptic.Smooth.realify_eq_of_real line 53
  9. lemma OAI.GlobalElliptic.conjugate_globalize line 59
  10. lemma OAI.GlobalElliptic.GluingData.conjugate_integer_bound line 68
  11. lemma OAI.GlobalElliptic.GluingData.embed_realify line 88
  12. lemma OAI.GlobalElliptic.GluingData.half_add_norm_le line 94
  13. lemma OAI.GlobalElliptic.GluingData.realify_integer_bound line 104