OAI/Analysis/Crouzeix/PhysicalFourier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Physical Fourier.

  1. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_complex_smul line 18
  2. lemma OAI.CrouzeixHilbert.Boundary.boundaryField_add line 32
  3. lemma OAI.CrouzeixHilbert.Boundary.boundaryField_smul line 40
  4. lemma OAI.CrouzeixHilbert.Boundary.boundaryField_zero line 48
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_complex line 62
  6. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionMoment_continuous_trace line 68
  7. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryKernel_moment line 73
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_complex_smul line 116
  9. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.scalarChannel line 125
  10. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionChannel line 128
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.kernelLp_fourier_pos line 132
  12. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalChannel line 152
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionChannel_negative line 159
  14. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_matrixFourier line 170
  15. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.boundaryCauchy_matrixLaurentMonomial line 212