3.6. Forms.Complete🔗

Jacobians.Forms.Complete — source

norm_localRep_sub_le_supNormK

Per-chart-chart uniform bound from chartNormK: for y ∈ shrunkChart x₀, |localRep (α - β) x₀ y| is bounded by chartNormK (α - β) x₀ ≤ supNormK (α - β).

theorem norm_localRep_sub_le_supNormK {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α β : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    {y : X} (hy : y ∈ shrunkChart (X := X) x₀) :
    ‖localRep α x₀ y - localRep β x₀ y‖ ≤ HolomorphicOneForms.supNormK (α - β)

cauchySeq_alpha_toFun_apply_symmL

For a supNormK-Cauchy sequence, the CLM value at each point is Cauchy. This uses the identity α.toFun y (e.symmL y 1) = localRep α x₀ y and the supNormK bound on localRep.

theorem cauchySeq_alpha_toFun_apply_symmL {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h_diff : ∀ ε > 0, ∃ N, ∀ n m, n ≥ N → m ≥ N →
      HolomorphicOneForms.supNormK (αs n - αs m) < ε)
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X)) {y : X}
    (hy : y ∈ shrunkChart (X := X) x₀) :
    CauchySeq (fun n : ℕ => localRep (αs n) x₀ y)

exists_subseq_bcf_tendsto_on_chartCover

Common bcf-convergent subsequence on chartCover. For any bounded sequence of sections (supNormK (αs n) ≤ 1), there is a strict-mono subsequence φ such that on each chart x₀ ∈ chartCover the bcf-image mkOfCompact ∘ localRepOnInnerShrunk (αs (φ n)) x₀ converges in BCF(innerShrunkChart x₀, ℂ).

theorem exists_subseq_bcf_tendsto_on_chartCover {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h : ∀ n, HolomorphicOneForms.supNormK (αs n) ≤ 1) :
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧
      ∀ x₀ ∈ (chartCover : Finset X),
        letI

cauchy_supNormK_of_bcf_tendsto

bcf-convergent on every chart ⇒ supNormK-Cauchy. Given a strict-mono subsequence φ such that the bcf-images on each innerShrunkChart x₀ converge, the subsequence is supNormK-Cauchy.

theorem cauchy_supNormK_of_bcf_tendsto {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (φ : ℕ → ℕ)
    (h_chart_conv : ∀ x₀ ∈ (chartCover : Finset X),
      letI := innerShrunkChart_compactSpace (X := X) x₀
      ∃ g : BoundedContinuousFunction (innerShrunkChart (X := X) x₀) ℂ,
        Tendsto
          (fun n : ℕ => BoundedContinuousFunction.mkOfCompact
            (localRepOnInnerShrunk (αs (φ n)) x₀))
          atTop (𝓝 g)) :
    ∀ ε > 0, ∃ N, ∀ n m, n ≥ N → m ≥ N →
      HolomorphicOneForms.supNormK (αs (φ n) - αs (φ m)) < ε

toFun_eq_localRep_smul

Coordinate identity. For y ∈ (trivializationAt … x₀).baseSet, α.toFun y equals (localRep α x₀ y) • φ where φ is the CLE T_y X ≃L[ℂ] ℂ from the trivialization.

theorem toFun_eq_localRep_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ y : X)
    (hy : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet) :
    letI e

cauchySeq_toFun_of_supNormK_cauchy

Pointwise CLM Cauchy. For a supNormK-Cauchy sequence and y ∈ shrunkChart x₀ (some x₀ ∈ chartCover), the CLM value (αs n).toFun y is Cauchy in T_y X →L[ℂ] ℂ.

Proof: the CLM L : ℂ →L[ℂ] (T_y X →L[ℂ] ℂ), c ↦ c • φ is Lipschitz (CLMs are Lipschitz). Since (αs n).toFun y = L (localRep (αs n) x₀ y) and localRep (αs n) x₀ y is Cauchy in ℂ, the image under L is Cauchy in the CLM space.

theorem cauchySeq_toFun_of_supNormK_cauchy {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h_diff : ∀ ε > 0, ∃ N, ∀ n m, n ≥ N → m ≥ N →
      HolomorphicOneForms.supNormK (αs n - αs m) < ε)
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    {y : X} (hy : y ∈ shrunkChart (X := X) x₀) :
    CauchySeq (fun n : ℕ => (αs n).toFun y)

exists_toFun_limit

Pointwise CLM limit of a supNormK-Cauchy sequence of sections.

theorem exists_toFun_limit {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h_diff : ∀ ε > 0, ∃ N, ∀ n m, n ≥ N → m ≥ N →
      HolomorphicOneForms.supNormK (αs n - αs m) < ε) :
    ∃ L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y,
      ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y))

localRep_tendsto_of_toFun_tendsto

Pointwise Tendsto of localReps from pointwise CLM Tendsto by continuity of evaluation at e.symmL ℂ y 1.

theorem localRep_tendsto_of_toFun_tendsto {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (αLim_toFun : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (αLim_toFun y)))
    (x₀ y : X) :
    letI e

norm_limit_localRep_le_one

Step 6a bound: for a bounded supNormK sequence with pointwise CLM limit L y, each scalar ‖L y (e.symmL ℂ y 1)‖ ≤ 1 at y ∈ shrunkChart x₀.

theorem norm_limit_localRep_le_one {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h : ∀ n, HolomorphicOneForms.supNormK (αs n) ≤ 1)
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    {y : X} (hy : y ∈ shrunkChart (X := X) x₀) :
    letI e

norm_localRep_sub_limit_le

Scalar-level convergence of localRep (αs n) x₀ y to L y (e.symmL ℂ y 1), uniformly over (x₀ ∈ chartCover, y ∈ shrunkChart x₀).

theorem norm_localRep_sub_limit_le {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (h_cauchy : ∀ ε > 0, ∃ N, ∀ n m, n ≥ N → m ≥ N →
      HolomorphicOneForms.supNormK (αs n - αs m) < ε)
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    (ε : ℝ) (hε : 0 < ε) :
    ∃ N, ∀ n, n ≥ N → ∀ (x₀ : X), x₀ ∈ (chartCover : Finset X) →
      ∀ (y : X), y ∈ shrunkChart (X := X) x₀ →
      letI e

tendstoLocallyUniformlyOn_pullback_on_innerChartOpen

Substep 1 of Path 2. Chart pullbacks of localRep converge locally uniformly on chart '' innerChartOpen x₀ to the pullback of y ↦ L y (e.symmL ℂ y 1), assuming bcf-convergence on innerShrunkChart x₀ and pointwise CLM Tendsto.

theorem tendstoLocallyUniformlyOn_pullback_on_innerChartOpen {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (g : letI := innerShrunkChart_compactSpace (X := X) x₀
      BoundedContinuousFunction (innerShrunkChart (X := X) x₀) ℂ)
    (hg : letI := innerShrunkChart_compactSpace (X := X) x₀
      Tendsto (fun n : ℕ =>
        BoundedContinuousFunction.mkOfCompact (localRepOnInnerShrunk (αs n) x₀))
        atTop (𝓝 g)) :
    letI e

analyticOn_limit_pullback_inner

Substep 2 of Path 2. The chart-pullback of y ↦ L y (e.symmL y 1) is analytic on chart '' innerChartOpen x₀ — feeds substep 3.

theorem analyticOn_limit_pullback_inner {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (g : letI := innerShrunkChart_compactSpace (X := X) x₀
      BoundedContinuousFunction (innerShrunkChart (X := X) x₀) ℂ)
    (hg : letI := innerShrunkChart_compactSpace (X := X) x₀
      Tendsto (fun n : ℕ =>
        BoundedContinuousFunction.mkOfCompact (localRepOnInnerShrunk (αs n) x₀))
        atTop (𝓝 g)) :
    letI e

contMDiffOn_limit_inner

Substep 3 of Path 2. Reverse of localRep_analyticOn_chartTarget: analytic pullback on chart '' innerChartOpen x₀ ⇒ ContMDiffOn ω of fun y => L y (e.symmL ℂ y 1) on innerChartOpen x₀.

theorem contMDiffOn_limit_inner {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (g : letI := innerShrunkChart_compactSpace (X := X) x₀
      BoundedContinuousFunction (innerShrunkChart (X := X) x₀) ℂ)
    (hg : letI := innerShrunkChart_compactSpace (X := X) x₀
      Tendsto (fun n : ℕ =>
        BoundedContinuousFunction.mkOfCompact (localRepOnInnerShrunk (αs n) x₀))
        atTop (𝓝 g)) :
    letI e

contMDiffOn_totalSpaceMk_L_inner

Substep 4 of Path 2. The pointwise CLM limit, packaged as a bundle-section, is ContMDiff ω on each innerChartOpen x₀ for x₀ ∈ chartCover.

Uses toFun_eq_localRep_smul to express L y = (scalar) • (CLE) and combines smoothness of the scalar (substep 3) with smoothness of the frame via clm_bundle_apply-style arguments. Concretely, we lift via Trivialization.contMDiffAt_section_iff on the Hom bundle, reducing section smoothness to smoothness of the inCoordinates CLM-valued function. For Trivial X ℂ-target, inCoordinates collapses to c(y) • (ContinuousLinearMap.id ℂ ℂ) where c(y) = L y (e.symmL y 1).

theorem contMDiffOn_totalSpaceMk_L_inner {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (αs : ℕ → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (L : (y : X) → TangentSpace 𝓘(ℂ, ℂ) y →L[ℂ] (Bundle.Trivial X ℂ) y)
    (hL : ∀ y : X, Tendsto (fun n : ℕ => (αs n).toFun y) atTop (𝓝 (L y)))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (g : letI := innerShrunkChart_compactSpace (X := X) x₀
      BoundedContinuousFunction (innerShrunkChart (X := X) x₀) ℂ)
    (hg : letI := innerShrunkChart_compactSpace (X := X) x₀
      Tendsto (fun n : ℕ =>
        BoundedContinuousFunction.mkOfCompact (localRepOnInnerShrunk (αs n) x₀))
        atTop (𝓝 g)) :
    ContMDiffOn 𝓘(ℂ, ℂ) (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ →L[ℂ] ℂ)) ω
      (fun y : X => TotalSpace.mk' (ℂ →L[ℂ] ℂ)
        (E := fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x)
        y (L y))
      (innerChartOpen (X := X) x₀)