ComplexifiedPolynomialOperator.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Complexification of the actual supported polynomial linearization.

def OAI.ClosedSurfaceR4.JetPolynomial.realFieldCLM line 14
def OAI.ClosedSurfaceR4.JetPolynomial.imagFieldCLM line 17
def OAI.ClosedSurfaceR4.JetPolynomial.Expression.complexVariationLM line 22
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.complexVariationLM_apply line 35
Source documentation
The bundled operator is the same complex first variation whose conjugated finite-jet estimates were proved above.
```
lemma complexVariationLM_apply {O : Set LowJet} {U : Set Base} {G : Base → Space} {e : Expression}
    (hO : IsOpen O) (hU : IsOpen U) (he : e.SmoothCoeffs O)
    (hG : ContDiff ℝ ∞ G) (hQ : Set.MapsTo (lowJet G) U O)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ U) (t : ℝ)
    (H : SupportedField (F := Fin 4 → ℂ) K) (p : Base) :
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.SupportedField