OAI/Analysis/Cotype/ComplexProjectionPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.complexProjectionProduct line 13
  2. theorem OAI.Cotype.complexProjectionProduct_differentiable line 17
  3. def OAI.Cotype.complexProjectionPolynomial line 26
  4. theorem OAI.Cotype.complexProjectionProduct_lift line 30
  5. theorem OAI.Cotype.complexProjectionPolynomial_real line 37
  6. theorem OAI.Cotype.complexProjectionPolynomial_differentiable line 46
  7. def OAI.Cotype.complexDualLiftCLM line 52
  8. theorem OAI.Cotype.complexDualLiftCLM_apply line 61
  9. theorem OAI.Cotype.complexProjectionPolynomial_deriv_zero line 64
  10. theorem OAI.Cotype.projectionLinearCoefficient_bound_of_complex_circle line 85