3.3. Forms.ChartNorm🔗

Jacobians.Forms.ChartNorm — source

HolomorphicOneForms.chartNormK

Bounded chart-local sup-norm: sup over the compact shrunkChart x₀.

noncomputable def HolomorphicOneForms.chartNormK {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) : ℝ

HolomorphicOneForms.chartNormK_bddAbove

The image of ‖localRep α x₀ ·‖ over shrunkChart x₀ is bounded above.

theorem HolomorphicOneForms.chartNormK_bddAbove {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) :
    BddAbove ((fun y : X => ‖localRep α x₀ y‖) '' shrunkChart (X := X) x₀)

HolomorphicOneForms.chartNormK_nonneg

chartNormK is non-negative.

theorem HolomorphicOneForms.chartNormK_nonneg {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) : 0 ≤ HolomorphicOneForms.chartNormK α x₀

HolomorphicOneForms.norm_localRep_le_chartNormK

Pointwise bound: ‖localRep α x₀ y‖ ≤ chartNormK α x₀ for y ∈ shrunkChart.

theorem HolomorphicOneForms.norm_localRep_le_chartNormK {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) {y : X} (hy : y ∈ shrunkChart (X := X) x₀) :
    ‖localRep α x₀ y‖ ≤ HolomorphicOneForms.chartNormK α x₀

HolomorphicOneForms.chartNormK_zero

chartNormK of the zero section is zero.

theorem HolomorphicOneForms.chartNormK_zero {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (x₀ : X) :
    HolomorphicOneForms.chartNormK
      (0 : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
        (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
      x₀ = 0

HolomorphicOneForms.chartNormK_add_le

Triangle inequality for chartNormK.

theorem HolomorphicOneForms.chartNormK_add_le {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) :
    HolomorphicOneForms.chartNormK (α + β) x₀ ≤
      HolomorphicOneForms.chartNormK α x₀ + HolomorphicOneForms.chartNormK β x₀

HolomorphicOneForms.chartNormK_smul_le

Sub-homogeneity: chartNormK (c • α) ≤ ‖c‖ * chartNormK α.

theorem HolomorphicOneForms.chartNormK_smul_le {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (c : ℂ)
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) :
    HolomorphicOneForms.chartNormK (c • α) x₀ ≤
      ‖c‖ * HolomorphicOneForms.chartNormK α x₀

HolomorphicOneForms.chartNormK_smul

Full homogeneity: chartNormK (c • α) = ‖c‖ * chartNormK α.

theorem HolomorphicOneForms.chartNormK_smul {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (c : ℂ)
    (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
    (x₀ : X) :
    HolomorphicOneForms.chartNormK (c • α) x₀ =
      ‖c‖ * HolomorphicOneForms.chartNormK α x₀