English
A trivial bundle with a fiber inner product is a continuous Riemannian bundle.
Русский
Тривиальное расслоение с нормированным произведением в фибре является непрерывным риммановым расслоением.
LaTeX
$$$\\text{IsContinuousRiemannianBundle } F_1 (Bundle.Trivial B F_1)$$$
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_self_comp_lt (x : B) {r : ℝ} (hr : 1 < r) :
∀ᶠ y in 𝓝 x, ‖((trivializationAt F E x).symmL ℝ x) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y)‖ < 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 `y`.
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 < δ ∧ (r' ^ 2)⁻¹ < 1 - δ * C :=
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.sub (tendsto_id.mul tendsto_const_nhds)
have B' : ∀ᶠ δ in 𝓝[>] 0, (r' ^ 2)⁻¹ < 1 - δ * C :=
by
apply (tendsto_order.1 B).1
simpa using inv_lt_one_of_one_lt₀ (by nlinarith)
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' x - g' y‖ ≤ δ := 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 ℝ y v
suffices ‖((trivializationAt F E x).symmL ℝ x) 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 hgy : g y v v = g' y w w :=
by
rw [inCoordinates_apply_eq₂ h'y h'y (Set.mem_univ _)]
have A : ((trivializationAt F E x).symm y) ((trivializationAt F E x).linearMapAt ℝ y v) = v :=
by
convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'y).symm_apply_apply v
rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'y]
rfl
simp [A, w]
have hgx : g x ((trivializationAt F E x).symm x w) ((trivializationAt F E x).symm x w) = g' x w w :=
by
rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
simp
rw [hgx, hgy]
-- get a good control for the norms of `w` in the model space, using continuity
have : g' x w w ≤ δ * C * g' x w w + g' y w w :=
calc
g' x w w
_ = (g' x - g' y) w w + g' y w w := by simp
_ ≤ ‖g' x - g' y‖ * ‖w‖ * ‖w‖ + g' y w w := by grw [← le_opNorm₂, ← Real.le_norm_self]
_ ≤ δ * ‖w‖ ^ 2 + g' y w w := by rw [pow_two, mul_assoc]; gcongr
_ ≤ δ * (‖(G : E x →L[ℝ] F)‖ * ‖G.symm w‖) ^ 2 + g' y w w :=
by
grw [← le_opNorm]
simp
_ = δ * C * ‖G.symm w‖ ^ 2 + g' y w w := by ring
_ = δ * C * g x (G.symm w) (G.symm w) + g' y w w := by simp [← real_inner_self_eq_norm_sq, hg]
_ = δ * C * g' x w w + g' y w w := by rw [← hgx]; rfl
have : (1 - δ * C) * g' x w w ≤ g' y w w := by linarith
rw [← (le_div_iff₀' (lt_of_le_of_lt (by positivity) hδ)), div_eq_inv_mul] at this
grw [this]
gcongr
· rw [← hgy, ← hg, real_inner_self_eq_norm_sq]
positivity
· exact inv_le_of_inv_le₀ (by positivity) hδ.le
