CC7: the 𝓘(ℝ, ℂ) bridge — real smoothness from holomorphy

Unit: surfaces-and-charts (docs/design/surfaces-and-charts.md §3.2, core-choices.md CC7).

𝓘(ℂ) and 𝓘(ℝ, ℂ) are different terms of different types, but both have toPartialEquiv = PartialEquiv.refl ℂ definitionally and share the same ChartedSpace ℂ X instance. This file provides, once and for all:

• instance isManifoldRealOfComplex : IsManifold 𝓘(ℝ, ℂ) ω X — a holomorphic atlas is ℝ-analytically compatible; IsManifold 𝓘(ℝ, ℂ) n X for every n (in particular ∞) then follows by instance search, unlocking SmoothPartitionOfUnity on X;
• the pinned rfl facts extChartAt_real_eq, coe_extChartAt_real_eq, writtenInExtChartAt_real_eq (consumed by dbar-solvability: the ℝ-charts ARE the ℂ-charts);
• ℝ-smoothness bridges contMDiffAt_real_iff_contDiffAt, contMDiffAt_real_iff_contDiffAt_writtenInExtChartAt;
• holomorphic ⇒ real-C^n: contMDiffAt_real_of_holomorphicAt, contMDiff_real_of_holomorphic, contMDiffOn_real_of_holomorphicOn;
• exists_smoothPartitionOfUnity on a compact T2 surface.

@[instance 100]

instance RS.isManifoldRealOfComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : IsManifold (modelWithCornersSelf ℝ ℂ) ⊤ X

CC7. A holomorphic atlas is ℝ-analytically compatible: ℂ-analytic transition maps are ℝ-analytic. Priority below the model-space instance so X := ℂ resolves to mathlib's instIsManifoldModelSpace first.

theorem RS.extChartAt_real_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) : extChartAt (modelWithCornersSelf ℝ ℂ) x = extChartAt (modelWithCornersSelf ℂ ℂ) x

CC7 pinned fact: the extended chart over 𝓘(ℝ, ℂ) IS the extended chart over 𝓘(ℂ).

theorem RS.coe_extChartAt_real_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) : ↑(extChartAt (modelWithCornersSelf ℝ ℂ) x) = ↑(extChartAt (modelWithCornersSelf ℂ ℂ) x)

Function-level variant.

theorem RS.writtenInExtChartAt_real_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} (x : X) : writtenInExtChartAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) x f = writtenInExtChartAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) x f

The two-model chart composites agree definitionally (consumed by dbar-solvability).

theorem RS.contMDiffAt_real_iff_contDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {n : WithTop ℕ∞} {f : X → ℂ} {x : X} : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) n f x ↔ ContDiffAt ℝ n (f ∘ ↑(extChartAt (modelWithCornersSelf ℂ ℂ) x).symm) (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x)

ℝ-smoothness bridge in the (shared) charts, f : X → ℂ.

theorem RS.contMDiffAt_real_iff_contDiffAt_writtenInExtChartAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {n : WithTop ℕ∞} {f : X → Y} {x : X} : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) n f x ↔ ContinuousAt f x ∧ ContDiffAt ℝ n (writtenInExtChartAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) x f) (↑(extChartAt (modelWithCornersSelf ℂ ℂ) x) x)

Two-chart ℝ-smoothness bridge, f : X → Y; the composite is written in the 𝓘(ℂ) charts (which are literally the 𝓘(ℝ, ℂ) charts).

theorem RS.contMDiffAt_real_of_holomorphicAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {n : WithTop ℕ∞} {f : X → Y} {x : X} (hf : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) n f x

Holomorphic ⇒ real-C^n, pointwise (n arbitrary, including ω and ∞).

theorem RS.contMDiff_real_of_holomorphic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {n : WithTop ℕ∞} {f : X → Y} (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) n f

Holomorphic ⇒ real-C^n, global.

theorem RS.contMDiffOn_real_of_holomorphicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {Y : Type u_2} [TopologicalSpace Y] [ChartedSpace ℂ Y] {n : WithTop ℕ∞} {f : X → Y} {s : Set X} (hs : IsOpen s) (hf : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f s) : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) n f s

Holomorphic ⇒ real-C^n on an open set.

theorem RS.exists_smoothPartitionOfUnity {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {ι : Type u_3} (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : Set.univ ⊆ ⋃ (i : ι), U i) : ∃ (p : SmoothPartitionOfUnity ι (modelWithCornersSelf ℝ ℂ) X), p.IsSubordinate U

Smooth partitions of unity subordinate to any open cover exist on a compact T2 surface (restated on our surface as a compile-time guarantee for the PoU-based units).