A machine-checked solution to the Jacobians challenge

3.11. Forms.Montel🔗

Jacobians.Forms.Montel — source

HolomorphicOneForms.supNormKAsAddGroupNorm

The AddGroupNorm structure on HolomorphicOneForms X.

noncomputable def HolomorphicOneForms.supNormKAsAddGroupNorm :
    AddGroupNorm (Jacobians.HolomorphicOneForms X) where

HolomorphicOneForms.normedAddCommGroup

HolomorphicOneForms X as a NormedAddCommGroup.

Non-instance: consumers opt in via letI or by promoting at a higher level (as done in Jacobians.HolomorphicForms).

@[reducible] noncomputable def HolomorphicOneForms.normedAddCommGroup :
    NormedAddCommGroup (Jacobians.HolomorphicOneForms X)

HolomorphicOneForms.normedSpace

HolomorphicOneForms X as a NormedSpace ℂ.

@[reducible] noncomputable def HolomorphicOneForms.normedSpace :
    letI

HolomorphicOneForms.exists_convergent_subseq_of_bounded

Bounded sequences in HOF X have convergent subsequences (bundle-level Montel's theorem). Fully proven and axiom-clean.

Given a bounded supNormK sequence of holomorphic 1-forms, there exists a supNormK-convergent subsequence with the limit in HOF X with supNormK limit ≤ 1.

Proof path (all ingredients proven in sibling modules):

  1. Per-chart Arzelà (B.8 in Compactness.lean) gives per-chart convergent subsequences in bcf(innerShrunkChart x₀, ℂ).

  2. Diagonal over finite chartCover gives a common subsequence with bcf-Cauchy per chart.

  3. exists_supNormK_le_const_sup_inner (chart-transition bound in ChartTransition.lean) lifts this to supNormK-Cauchy.

  4. Define αLim.toFun as the pointwise CLM limit (CLM space complete).

  5. Show αLim is a ContMDiffSection ω via chart-wise analyticity of the pullback, using analyticOn_of_pullback_tendsto_locally_uniformly from Compactness.lean + chart characterization of ContMDiff.

  6. Show αs(φ k) → αLim in supNormK and supNormK αLim ≤ 1.

Step 5 is the bundle-level "uniform limit of holomorphic sections is holomorphic"; it is discharged in Complete.lean via contMDiffOn_totalSpaceMk_L_inner.

theorem HolomorphicOneForms.exists_convergent_subseq_of_bounded
    (αs : ℕ → Jacobians.HolomorphicOneForms X)
    (h : ∀ n, HolomorphicOneForms.supNormK (αs n) ≤ 1) :
    letI

HolomorphicOneForms.closedBall_isCompact

Montel's closedBall is compact, under the canonical supNormK-based normed structure. With exists_convergent_subseq_of_bounded supplying the structural bundle-reconstruction piece, this closes via sequential compactness.

Takes no typeclass arguments — uses the specific supNormK-based norm (via letI in the type). At call sites where the canonical HolomorphicOneForms.normedAddCommGroup is in scope as an instance, types unify.

theorem HolomorphicOneForms.closedBall_isCompact :
    letI