OAI/Analysis/Crouzeix/PhysicalProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Physical Projection.

  1. def OAI.CrouzeixHilbert.Boundary.boundaryFieldCLM line 19
  2. lemma OAI.CrouzeixHilbert.Boundary.boundaryFieldCLM_apply line 23
  3. lemma OAI.CrouzeixHilbert.Boundary.boundaryField_sum line 26
  4. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalPolynomial line 38
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_physicalPolynomial line 41
  6. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.polynomialCircle line 46
  7. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalPolynomialTrace line 49
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_polynomialCircle line 54
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalPolynomial_inside line 74
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.cauchy_inverse_q_zero line 93
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalPolynomial_of_power_split line 103
  12. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_physical_power line 141