3.12. Forms.SupNorm🔗

Jacobians.Forms.SupNorm — source

HolomorphicOneForms.supNormK

The assembled sup-norm on HolomorphicOneForms X: sup over chartCover of per-chart chartNormK.

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

HolomorphicOneForms.supNormK_nonneg

supNormK is non-negative.

theorem HolomorphicOneForms.supNormK_nonneg {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)) :
    0 ≤ HolomorphicOneForms.supNormK α

HolomorphicOneForms.chartNormK_le_supNormK

Chart-local bound via supNormK.

theorem HolomorphicOneForms.chartNormK_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)) :
    HolomorphicOneForms.chartNormK α x₀ ≤ HolomorphicOneForms.supNormK α

HolomorphicOneForms.norm_localRep_le_supNormK

Pointwise bound via supNormK.

theorem HolomorphicOneForms.norm_localRep_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‖ ≤ HolomorphicOneForms.supNormK α

HolomorphicOneForms.supNormK_zero

supNormK of zero is zero.

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

HolomorphicOneForms.supNormK_add_le

Triangle inequality for supNormK.

theorem HolomorphicOneForms.supNormK_add_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)) :
    HolomorphicOneForms.supNormK (α + β) ≤
      HolomorphicOneForms.supNormK α + HolomorphicOneForms.supNormK β

HolomorphicOneForms.supNormK_smul

Homogeneity of supNormK.

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

HolomorphicOneForms.supNormK_neg

Negation invariance: supNormK (-α) = supNormK α.

theorem HolomorphicOneForms.supNormK_neg {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)) :
    HolomorphicOneForms.supNormK (-α) = HolomorphicOneForms.supNormK α

HolomorphicOneForms.localRep_eq_zero_of_chartNormK_eq_zero

If chartNormK α x₀ = 0 then localRep α x₀ y = 0 for y ∈ shrunkChart x₀.

theorem HolomorphicOneForms.localRep_eq_zero_of_chartNormK_eq_zero {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) (h : HolomorphicOneForms.chartNormK α x₀ = 0)
    (y : X) (hy : y ∈ shrunkChart (X := X) x₀) :
    localRep α x₀ y = 0

HolomorphicOneForms.chartNormK_eq_zero_of_supNormK_eq_zero

If supNormK α = 0 then chartNormK α x = 0 for every x ∈ chartCover.

theorem HolomorphicOneForms.chartNormK_eq_zero_of_supNormK_eq_zero {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))
    (h : HolomorphicOneForms.supNormK α = 0)
    (x : X) (hx : x ∈ (chartCover : Finset X)) :
    HolomorphicOneForms.chartNormK α x = 0

HolomorphicOneForms.localRep_eq_zero_of_supNormK_eq_zero

supNormK α = 0 forces localRep α x₀ y = 0 for every x₀ ∈ chartCover and y ∈ shrunkChart x₀.

theorem HolomorphicOneForms.localRep_eq_zero_of_supNormK_eq_zero {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))
    (h : HolomorphicOneForms.supNormK α = 0)
    (x₀ : X) (hx₀ : x₀ ∈ (chartCover : Finset X))
    (y : X) (hy : y ∈ shrunkChart (X := X) x₀) :
    localRep α x₀ y = 0

alpha_toFun_eq_zero_of_localRep_eq_zero

If the local representative of α vanishes at y ∈ baseSet of the trivialization at x₀, then α.toFun y = 0 as a continuous linear map.

This uses that T_y X ≃L[ℂ] ℂ on the trivialization base set (X is charted over ℂ, so tangent spaces are 1-dim over ℂ), and that the image of 1 under (φ.symm) is a nonzero vector — a CLM vanishing on a spanning vector is 0.

theorem alpha_toFun_eq_zero_of_localRep_eq_zero {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)
    (h : localRep α x₀ y = 0) :
    α.toFun y = 0

HolomorphicOneForms.eq_zero_of_supNormK_eq_zero

Positive-definiteness: supNormK α = 0 → α = 0.

theorem HolomorphicOneForms.eq_zero_of_supNormK_eq_zero {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))
    (h : HolomorphicOneForms.supNormK α = 0) :
    α = 0