OAI/Geometry/RCD/Sobolev/EulerPairingLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.inner_tendsto_zero_of_norm_tendsto_zero line 16

   Source documentation

   A bounded test kills an error tending to zero in L2. The spaces may vary with the rescaling index.

   theorem inner_tendsto_zero_of_norm_tendsto_zero
       {H : ℕ → Type*} [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℝ (H i)]
       (p e : ∀ i, H i) {C : ℝ} (hp : ∀ i, ‖p i‖ ≤ C)
       (he : Tendsto (fun i => ‖e i‖) atTop (𝓝 0)) :
       Tendsto (fun i => ⟪p i, e i⟫_ℝ) atTop (𝓝 0) := by
   …

2. theorem OAI.RegularPointCoordinates.euler_pairing_limit line 29

   Source documentation

   Every term in the exact projected equation has a separate weak or strong convergence input. This calculation identifies its limit without assuming a limiting Euler equation.

   theorem euler_pairing_limit {n : ℕ}
       {H : ℕ → Type*} [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℝ (H i)]
       (p d w one e : ∀ i, H i) (u : ∀ i, Fin n → H i)
       (ell : ℕ → Fin n → ℝ) (k : ℕ → ℝ)
       (hid : ∀ i, d i = w i + ∑ j, ell i j • u i j + k i • one i + e i)
       {C D W O K : ℝ} {L U : Fin n → ℝ}
       (hp : ∀ i, ‖p i‖ ≤ C) (he : Tendsto (fun i => ‖e i‖) atTop (𝓝 0))
       (hd : Tendsto (fun i => ⟪p i, d i⟫_ℝ) atTop (𝓝 D))
       (hw : Tendsto (fun i => ⟪p i, w i⟫_ℝ) atTop (𝓝 W))
       (ho : Tendsto (fun i => ⟪p i, one i⟫_ℝ) atTop (𝓝 O))
       (hu : ∀ j, Tendsto (fun i => ⟪p i, u i j⟫_ℝ) atTop (𝓝 (U j)))
       (hl : ∀ j, Tendsto (fun i => ell i j) atTop (𝓝 (L j)))
   …