5.4. Surface.ContMDiffOmegaAnalytic🔗

Jacobians.Surface.ContMDiffOmegaAnalytic — source

contMDiffAt_omega_analyticAt_chart_pullback

Bridge ContMDiffAt … ω → AnalyticAt ℂ on chart pullbacks. For f : X → Y real-analytic at x between complex-analytic manifolds modelled on ℂ (with corners model 𝓘(ℂ)), the chart-pulled-back representation (chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm is AnalyticAt ℂ at the chart image (chartAt ℂ x) x.

This is the missing classical hypothesis flagged in AnalyticFiberDiscrete.lean.

theorem contMDiffAt_omega_analyticAt_chart_pullback
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y} {x : X}
    (h : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω f x) :
    AnalyticAt ℂ ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm)
      ((chartAt ℂ x) x)

contMDiff_omega_analyticAt_chart_pullback

ContMDiff version. If f is C^ω everywhere, then for every x the chart pullback is AnalyticAt.

theorem contMDiff_omega_analyticAt_chart_pullback
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y} (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x : X) :
    AnalyticAt ℂ ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm)
      ((chartAt ℂ x) x)