eventually_norm_symmL_trivializationAt_comp_self_lt

English

Let F be a normed vector space and E a fibre bundle over a base B with a continuous Riemannian structure on the fibres. For every x in B and every r > 1 there exists a neighbourhood U of x such that for all y in U the coordinate change from the fibre at x to the fibre at y, induced by the trivialization at x, distorts the norm by a factor less than r. In particular, the local chart is arbitrarily close to an isometry as y approaches x.

Русский

Пусть F — нормированное векторное пространство, E — волокно над базой B с непрерывной римановой структурой на волокнах. Для каждого x ∈ B и каждого r > 1 существует окрестность U(x) such that for all y ∈ U(x) переходная линейная карта между волокнами E_x и E_y, заданная тривиализацией в x, имеет операторную норму меньше r. Следовательно, локальная координатная карта близка к изометрии при y → x.

LaTeX

$$$$\forall x \in B,\ \forall r>1,\ \exists U \ni x:\ \forall y \in U,\ \|T_{x\to y}\| < r,$$$$

Lean4

/-- In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at
a point distort the norm by a factor arbitrarily close to 1. -/
theorem eventually_norm_symmL_trivializationAt_comp_self_lt (x : B) {r : ℝ} (hr : 1 < r) :
    ∀ᶠ y in 𝓝 x, ‖((trivializationAt F E x).symmL ℝ y) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ x)‖ < r :=
  by
  /- We will expand the definition of continuity of the inner product structure, in the chart.
    Denote `g' x` the metric in the fiber of `x`, read in the chart. For `y` close to `x`, then
    `g' y` and `g' x` are close. The inequality we have to prove reduces to comparing
    `g' y w w` and `g' x w w`, where `w` is the image in the chart of a tangent vector `v` at `x`.
    Their difference is controlled by `δ ‖w‖ ^ 2` for any small `δ > 0`. To conclude, we argue that
    `‖w‖` is comparable to the norm inside the fiber over `x`, i.e., `g' x w w`, because there
    is a continuous linear equivalence between these two spaces by definition of vector bundles. -/

  obtain ⟨r', hr', r'r⟩ : ∃ r', 1 < r' ∧ r' < r := exists_between hr
  have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
  let G := (trivializationAt F E x).continuousLinearEquivAt ℝ x h'x
  let C :=
    (‖(G : E x →L[ℝ] F)‖) ^
      2
        -- choose `δ` small enough that the computation below works when the metrics at `x` and `y`
          -- are `δ` close. When writing this proof, I have followed my nose in the computation, and
          -- recorded only in the end how small `δ` needs to be. The reader should skip the precise
          -- condition for now, as it doesn't give any useful insight.

  obtain ⟨δ, δpos, h'δ⟩ : ∃ δ, 0 < δ ∧ (1 + δ * C) < r' ^ 2 :=
    by
    have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
    have B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C)) :=
      by
      apply tendsto_inf_left
      exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
    have B' : ∀ᶠ δ in 𝓝[>] 0, 1 + δ * C < r' ^ 2 :=
      by
      apply (tendsto_order.1 B).2
      simpa using hr'.trans_le (le_abs_self _)
    exact (A.and B').exists
  rcases h.exists_continuous with ⟨g, g_cont, hg⟩
  let g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
  have hg' : ContinuousAt g' x := by
    have W := g_cont.continuousAt (x := x)
    simp only [continuousAt_hom_bundle] at W
    exact W.2
  have : ∀ᶠ y in 𝓝 x, dist (g' y) (g' x) < δ :=
    by
    rw [Metric.continuousAt_iff'] at hg'
    apply hg' _ δpos
  filter_upwards [this, (trivializationAt F E x).open_baseSet.mem_nhds h'x] with y hy h'y
  have : ‖g' y - g' x‖ ≤ δ := by rw [← dist_eq_norm]; exact hy.le
  apply (opNorm_le_bound _ (by linarith) (fun v ↦ ?_)).trans_lt r'r
  let w := (trivializationAt F E x).continuousLinearMapAt ℝ x v
  suffices ‖((trivializationAt F E x).symmL ℝ y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2 from
    le_of_sq_le_sq (by simpa [mul_pow]) (by positivity)
  simp only [Trivialization.symmL_apply, ← real_inner_self_eq_norm_sq, hg]
  have hgx : g x v v = g' x w w :=
    by
    rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
    have A : ((trivializationAt F E x).symm x) ((trivializationAt F E x).linearMapAt ℝ x v) = v :=
      by
      convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).symm_apply_apply v
      rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
      rfl
    simp [A, w]
  have hgy : g y ((trivializationAt F E x).symm y w) ((trivializationAt F E x).symm y w) = g' y w w :=
    by
    rw [inCoordinates_apply_eq₂ h'y h'y (Set.mem_univ _)]
    simp
  rw [hgx, hgy]
    -- get a good control for the norms of `w` in the model space, using continuity

  calc
    g' y w w
    _ = (g' y - g' x) w w + g' x w w := by simp
    _ ≤ ‖g' y - g' x‖ * ‖w‖ * ‖w‖ + g' x w w := by grw [← le_opNorm₂, ← Real.le_norm_self]
    _ ≤ δ * ‖w‖ ^ 2 + g' x w w := by rw [pow_two, mul_assoc]; gcongr
    _ ≤ δ * (‖(G : E x →L[ℝ] F)‖ * ‖G.symm w‖) ^ 2 + g' x w w :=
      by
      grw [← le_opNorm]
      simp
    _ = δ * C * ‖G.symm w‖ ^ 2 + g' x w w := by ring
    _ = δ * C * g x (G.symm w) (G.symm w) + g' x w w := by simp [← real_inner_self_eq_norm_sq, hg]
    _ = δ * C * g' x w w + g' x w w := by
      congr
      rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
      simp only [Trivial.fiberBundle_trivializationAt', Trivial.linearMapAt_trivialization, LinearMap.id_coe, id_eq, w]
      rfl
    _ = (1 + δ * C) * g' x w w := by ring
    _ ≤ r' ^ 2 * g' x w w := by
      gcongr
      rw [← hgx, ← hg, real_inner_self_eq_norm_sq]
      positivity

Похожие утверждения