3.4. Forms.ChartTransition🔗

Jacobians.Forms.ChartTransition — source

chartTransitionFactor

The chart-transition factor between two tangent-bundle trivializations, evaluated at a point y. Equals 1 by convention if y is not in both base sets.

noncomputable def chartTransitionFactor {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x₀' y : X) : ℂ

chartTransitionFactor_ne_zero

The chart-transition factor is nonzero (a CLE sends nonzero to nonzero).

theorem chartTransitionFactor_ne_zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x₀' y : X) :
    chartTransitionFactor (X := X) x₀ x₀' y ≠ 0

symmL_apply_chartTransitionFactor

Key identity: e.symmL y (c(y)) = e'.symmL y 1, where c(y) = chartTransitionFactor x₀ x₀' y, for y in both base sets.

theorem symmL_apply_chartTransitionFactor {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x₀' y : X)
    (hy₀' : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀').baseSet)
    (hy₀ : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).symmL ℂ y
      (chartTransitionFactor (X := X) x₀ x₀' y) =
      (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀').symmL ℂ y 1

localRep_chart_transition

Chart-transition relation for localRep: localRep α x₀' y = c(y) · localRep α x₀ y with c = chartTransitionFactor.

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

continuousOn_chartTransitionFactor

Continuity of chartTransitionFactor on the overlap of two base sets.

theorem continuousOn_chartTransitionFactor {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x₀' : X) :
    ContinuousOn (chartTransitionFactor (X := X) x₀ x₀')
      ((trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀').baseSet ∩
        (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) x₀).baseSet)

exists_pairwise_chart_transition_bound

Pairwise bound: for each chart pair (x₀, x₀') ∈ chartCover², there's a universal constant M ≥ 0 such that for any α and any point y in the overlap shrunkChart x₀ ∩ innerShrunkChart x₀', ‖localRep α x₀ y‖ ≤ M · ‖localRep α x₀' y‖.

Proof: 1/‖chartTransitionFactor x₀ x₀' y‖ is continuous and bounded on the compact overlap (since c ≠ 0 there); take the sup as M.

theorem exists_pairwise_chart_transition_bound {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (x₀ x₀' : X) (hx₀ : x₀ ∈ (chartCover : Finset X))
    (hx₀' : x₀' ∈ (chartCover : Finset X)) :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
      (y : X), y ∈ shrunkChart (X := X) x₀ → y ∈ innerShrunkChart (X := X) x₀' →
        ‖localRep α x₀ y‖ ≤ M * ‖localRep α x₀' y‖

exists_global_chart_transition_bound

Global chart-transition bound (pointwise form). There is a universal constant M ≥ 0 such that for any α, for any x₀ ∈ chartCover and any y ∈ shrunkChart x₀, there exists x₀' ∈ chartCover with y ∈ innerShrunkChart x₀' and ‖localRep α x₀ y‖ ≤ M · ‖localRep α x₀' y‖.

theorem exists_global_chart_transition_bound {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x))
      (x₀ : X), x₀ ∈ (chartCover : Finset X) →
        ∀ (y : X), y ∈ shrunkChart (X := X) x₀ →
          ∃ (x₀' : X) (_hx₀' : x₀' ∈ (chartCover : Finset X))
            (_hy' : y ∈ innerShrunkChart (X := X) x₀'),
            ‖localRep α x₀ y‖ ≤ M * ‖localRep α x₀' y‖

exists_supNormK_le_const_sup_inner

Chart-transition supNormK bound. There exists a universal constant M ≥ 0 such that for any α, supNormK α ≤ M · (max over chartCover of sSup of ‖localRep α x₀'·‖ on innerShrunkChart x₀').

This is the supNormK form of exists_global_chart_transition_bound, obtained by taking sup over y of the pointwise bound.

theorem exists_supNormK_le_const_sup_inner {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    ∃ M : ℝ, 0 ≤ M ∧ ∀ (α : ContMDiffSection 𝓘(ℂ, ℂ) (ℂ →L[ℂ] ℂ) ω
      (fun x : X => TangentSpace 𝓘(ℂ, ℂ) x →L[ℂ] (Bundle.Trivial X ℂ) x)),
      HolomorphicOneForms.supNormK α ≤
        M * (chartCover : Finset X).sup' chartCover_nonempty
          (fun x₀' => sSup ((fun y : X => ‖localRep α x₀' y‖) ''
            innerShrunkChart (X := X) x₀'))