A machine-checked solution to the Jacobians challenge

3.5. Forms.Compactness🔗

Jacobians.Forms.Compactness — source

shrunkChart_subset_baseSet

shrunkChart x₀ is contained in the trivialization base set at x₀, provided x₀ ∈ chartCover.

theorem shrunkChart_subset_baseSet {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    shrunkChart (X := X) x₀ ⊆
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet

innerShrunkChart_subset_baseSet

theorem innerShrunkChart_subset_baseSet {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (x₀ : X)
    (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    innerShrunkChart (X := X) x₀ ⊆
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet

localRep_continuousOn_innerShrunkChart

theorem localRep_continuousOn_innerShrunkChart {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    ContinuousOn (localRep α x₀) (innerShrunkChart (X := X) x₀)

innerShrunkChart_compactSpace

theorem innerShrunkChart_compactSpace {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x₀ : X) :
    CompactSpace (innerShrunkChart (X := X) x₀)

localRepOnInnerShrunk

localRep α x₀ bundled as a continuous map on the compact inner innerShrunkChart x₀. Fallback to constant zero for x₀ ∉ chartCover (where innerShrunkChart x₀ = ∅).

noncomputable def localRepOnInnerShrunk {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) : C(innerShrunkChart (X := X) x₀, ℂ)

localRepOnInnerShrunk_apply

theorem localRepOnInnerShrunk_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace 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 : innerShrunkChart (X := X) x₀) :
    localRepOnInnerShrunk α x₀ y = localRep α x₀ (y : X)

norm_localRepOnInnerShrunk_le_supNormK

Component-wise bound for the inner version: same supNormK bound as outer, since innerShrunkChart ⊆ shrunkChart and the norm bound on outer lifts to inner.

theorem norm_localRepOnInnerShrunk_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)) :
    letI

norm_localRep_le_supNormK_on_chartOpen

|localRep α x₀| ≤ supNormK α on the OPEN layer chartOpen x₀ (for x₀ ∈ chartCover). Since chartOpen x₀ ⊆ shrunkChart x₀, this is immediate from norm_localRep_le_supNormK.

theorem norm_localRep_le_supNormK_on_chartOpen {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 ∈ chartOpen (X := X) x₀) :
    ‖localRep α x₀ y‖ ≤ HolomorphicOneForms.supNormK α

chartOpen_subset_source

chartOpen x₀ is contained in the chart source for x₀ ∈ chartCover.

theorem chartOpen_subset_source {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    chartOpen (X := X) x₀ ⊆ (chartAt ℂ x₀).source

baseSet_eq_chartAt_source

The trivialization base set at x₀ equals (chartAt ℂ x₀).source (specialization of TangentBundle.trivializationAt_baseSet).

theorem baseSet_eq_chartAt_source {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ : X) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet =
      (chartAt ℂ x₀).source

contMDiffOn_frame

The constant-1 tangent-frame section y ↦ (trivializationAt …).symmL ℂ y 1 is smooth as a bundle section on the trivialization's base set. Proof: via Trivialization.contMDiffOn_section_baseSet_iff, equivalent to smoothness of the trivialization representative, which equals the constant 1 : ℂ on the base set.

theorem contMDiffOn_frame {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (x₀ : X) :
    ContMDiffOn 𝓘(ℂ, ℂ) (𝓘(ℂ, ℂ).prod 𝓘(ℂ, ℂ)) ω
      (fun y : X => TotalSpace.mk' ℂ
        (E := fun x : X => TangentSpace 𝓘(ℂ, ℂ) x) y
        ((trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).symmL ℂ y 1))
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet

localRep_contMDiffOn

Scalar smoothness of localRep α x₀ as a function X → ℂ on the chart source (= trivialization base set). Combines α.contMDiff_toFun, contMDiffOn_frame, and ContMDiffOn.clm_bundle_apply via scalar extraction on the Trivial bundle.

theorem localRep_contMDiffOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) :
    ContMDiffOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ω (localRep α x₀)
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet

localRep_analyticOn_chartTarget

Step B.3 — the holomorphicity bridge. In chart coordinates at x₀, the local representative of a holomorphic 1-form α is analytic on the chart target.

Proof chain:

  1. localRep_contMDiffOn gives ContMDiffOn ω on the chart source.

  2. contMDiffOn_iff reduces this to ContDiffOn ℂ ω in chart coordinates (using that ℂ's extChartAt is essentially the identity).

  3. contDiffOn_omega_iff_analyticOn on the open chart target promotes ContDiffOn ω ⇒ AnalyticOn.

theorem localRep_analyticOn_chartTarget {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) :
    AnalyticOn ℂ (fun z : ℂ => localRep α x₀ ((chartAt ℂ x₀).symm z))
      (chartAt ℂ x₀).target

isOpen_chart_image_chartOpen

The chart image of chartOpen x₀ is open in ℂ.

theorem isOpen_chart_image_chartOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    IsOpen ((chartAt ℂ x₀) '' chartOpen (X := X) x₀)

chart_image_chartOpen_subset_target

The chart image of chartOpen x₀ sits inside the chart target.

theorem chart_image_chartOpen_subset_target {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    (chartAt ℂ x₀) '' chartOpen (X := X) x₀ ⊆ (chartAt ℂ x₀).target

innerChartOpen_subset_source

innerChartOpen x₀ ⊆ (chartAt ℂ x₀).source for x₀ ∈ chartCover. innerChartOpen ⊆ closure(innerChartOpen) ⊆ chartOpen ⊆ chartAt source.

theorem innerChartOpen_subset_source {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    innerChartOpen (X := X) x₀ ⊆ (chartAt ℂ x₀).source

isOpen_chart_image_innerChartOpen

The chart image of innerChartOpen x₀ is open in ℂ.

theorem isOpen_chart_image_innerChartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    IsOpen ((chartAt ℂ x₀) '' innerChartOpen (X := X) x₀)

chart_image_innerChartOpen_subset_target

The chart image of innerChartOpen x₀ sits inside the chart target.

theorem chart_image_innerChartOpen_subset_target {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    (chartAt ℂ x₀) '' innerChartOpen (X := X) x₀ ⊆ (chartAt ℂ x₀).target

localRep_analyticOn_chart_image_innerChartOpen

Pullback analyticity on the chart image of innerChartOpen x₀.

theorem localRep_analyticOn_chart_image_innerChartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    AnalyticOn ℂ (fun z : ℂ => localRep α x₀ ((chartAt ℂ x₀).symm z))
      ((chartAt ℂ x₀) '' innerChartOpen (X := X) x₀)

localRep_analyticOn_chart_image_chartOpen

Pullback analyticity on the chart image of chartOpen x₀. Direct specialization of localRep_analyticOn_chartTarget via AnalyticOn.mono.

theorem localRep_analyticOn_chart_image_chartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    AnalyticOn ℂ (fun z : ℂ => localRep α x₀ ((chartAt ℂ x₀).symm z))
      ((chartAt ℂ x₀) '' chartOpen (X := X) x₀)

norm_localRep_pullback_le_supNormK_on_chart_image_chartOpen

The pullback localRep α x₀ ∘ chart.symm is bounded by supNormK α on the chart image of chartOpen x₀.

theorem norm_localRep_pullback_le_supNormK_on_chart_image_chartOpen {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))
    {z : ℂ} (hz : z ∈ (chartAt ℂ x₀) '' chartOpen (X := X) x₀) :
    ‖localRep α x₀ ((chartAt ℂ x₀).symm z)‖ ≤ HolomorphicOneForms.supNormK α

exists_cauchy_deriv_bound

Cauchy estimate on a compact subset of an open set: for f analytic on U with ‖f‖ ≤ C, ‖deriv f z‖ ≤ L · C for all z ∈ K, with L = 1/δ depending only on K ⊂ U.

theorem exists_cauchy_deriv_bound
    {U K : Set ℂ} (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U) :
    ∃ L : ℝ, 0 < L ∧ ∀ (f : ℂ → ℂ), AnalyticOn ℂ f U → ∀ C : ℝ,
      (∀ z ∈ U, ‖f z‖ ≤ C) → ∀ z ∈ K, ‖deriv f z‖ ≤ L * C

analyticOn_of_tendstoLocallyUniformlyOn

Uniform-local limits of analytic functions are analytic. A locally-uniform limit of AnalyticOn functions on an open U ⊆ ℂ is itself AnalyticOn U.

theorem analyticOn_of_tendstoLocallyUniformlyOn
    {ι : Type*} {U : Set ℂ} {F : ι → ℂ → ℂ} {f : ℂ → ℂ}
    {φ : Filter ι} [φ.NeBot]
    (hU : IsOpen U)
    (hlim : TendstoLocallyUniformlyOn F f φ U)
    (hF : ∀ᶠ n in φ, AnalyticOn ℂ (F n) U) :
    AnalyticOn ℂ f U

analyticOn_of_pullback_tendsto_locally_uniformly_inner

Chart-pullback analytic limit on innerChartOpen. Inner-open variant of analyticOn_of_pullback_tendsto_locally_uniformly. Needed when we can only establish locally uniform convergence on the smaller chart '' innerChartOpen x₀ (as arises from bcf-convergence on the compact innerShrunkChart x₀, restricted to its open interior).

theorem analyticOn_of_pullback_tendsto_locally_uniformly_inner {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {ι : Type*} {φ : Filter ι} [φ.NeBot]
    (αf : ι → ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (g : ℂ → ℂ)
    (hconv : TendstoLocallyUniformlyOn
      (fun n : ι => fun z : ℂ => localRep (αf n) x₀ ((chartAt ℂ x₀).symm z))
      g φ ((chartAt ℂ x₀) '' innerChartOpen (X := X) x₀)) :
    AnalyticOn ℂ g ((chartAt ℂ x₀) '' innerChartOpen (X := X) x₀)

exists_cauchy_lipschitz_bound

Uniform Lipschitz bound for a family of analytic functions bounded on an open set, restricted to a convex compact subset.

theorem exists_cauchy_lipschitz_bound
    {U K : Set ℂ} (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U)
    (hKconv : Convex ℝ K) :
    ∃ L : ℝ, 0 < L ∧ ∀ (f : ℂ → ℂ), AnalyticOn ℂ f U → ∀ C : ℝ,
      (∀ z ∈ U, ‖f z‖ ≤ C) → ∀ z ∈ K, ∀ w ∈ K, ‖f z - f w‖ ≤ L * C * ‖z - w‖

uniformEquicontinuousOn_of_bounded_analyticOn

A bounded family of analytic functions on open U is uniformly equicontinuous on any convex compact K ⊂ U.

Note: requires 0 ≤ C (trivially true if U is nonempty — take any z ∈ U and use ‖f z‖ ≤ C; stated explicitly here to avoid case-splitting).

theorem uniformEquicontinuousOn_of_bounded_analyticOn
    {ι : Type*} {U K : Set ℂ} {f : ι → ℂ → ℂ} {C : ℝ}
    (hU : IsOpen U) (hKcpt : IsCompact K) (hKU : K ⊆ U) (hKconv : Convex ℝ K)
    (hCnn : 0 ≤ C)
    (hf : ∀ i, AnalyticOn ℂ (f i) U)
    (hfb : ∀ i, ∀ z ∈ U, ‖f i z‖ ≤ C) :
    UniformEquicontinuousOn f K

norm_localRep_pullback_le_of_supNormK_le

For a holomorphic 1-form bounded by M under supNormK, the pullback through the chart at x₀ is bounded by M on chart '' chartOpen x₀. Packaging of earlier bridge lemmas.

theorem norm_localRep_pullback_le_of_supNormK_le {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))
    {M : ℝ} (hαM : HolomorphicOneForms.supNormK α ≤ M)
    {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    {z : ℂ} (hz : z ∈ (chartAt ℂ x₀) '' chartOpen (X := X) x₀) :
    ‖localRep α x₀ ((chartAt ℂ x₀).symm z)‖ ≤ M

equicontinuousAt_localRep_on_innerShrunkChart

Equicontinuity of the inner family. For each y₀ : innerShrunkChart x₀ and ε > 0, there's an X-nbhd V of y₀.val with: ‖localRep α x₀ y - localRep α x₀ y₀.val‖ < ε for all α with supNormK α ≤ M and all y ∈ V ∩ innerShrunkChart x₀.

Proof: via B.6 on a closed ball closedBall (chart y₀) r strictly inside the open chart '' chartOpen x₀, then transfer through chart continuity at y₀.

theorem equicontinuousAt_localRep_on_innerShrunkChart {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (M : ℝ) (hMnn : 0 ≤ M) {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X))
    (y₀ : X) (hy₀ : y₀ ∈ innerShrunkChart (X := X) x₀) :
    ∀ ε > 0, ∃ V ∈ 𝓝 y₀, ∀ y ∈ V, ∀ α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x),
        HolomorphicOneForms.supNormK α ≤ M →
        y ∈ innerShrunkChart (X := X) x₀ →
        ‖localRep α x₀ y - localRep α x₀ y₀‖ ≤ ε

equicontinuous_localRep_inner_family

Equicontinuous family on innerShrunkChart x₀. The family indexed by α with supNormK α ≤ M of functions (y : innerShrunkChart x₀) ↦ localRep α x₀ y.val is Equicontinuous, i.e., pointwise equicontinuous at every point. Derived from equicontinuousAt_localRep_on_innerShrunkChart by packaging the neighborhood-in-X witness into the subtype neighborhood via nhds_subtype.

theorem equicontinuous_localRep_inner_family {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (M : ℝ) (hMnn : 0 ≤ M) {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    Equicontinuous
      (fun α : {α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
          (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x) //
          HolomorphicOneForms.supNormK α ≤ M} =>
        fun y : innerShrunkChart (X := X) x₀ => localRep α.1 x₀ (y : X))

isCompact_closure_image_inner_bcf

Per-chart relative compactness. The image of the supNormK-M-ball under α ↦ mkOfCompact ∘ localRepOnInnerShrunk α x₀ has compact closure in innerShrunkChart x₀ →ᵇ ℂ.

theorem isCompact_closure_image_inner_bcf {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (M : ℝ) (hMnn : 0 ≤ M) {x₀ : X} (hx₀ : x₀ ∈ (chartCover : Finset X)) :
    letI