ScalarH2Closure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the first and second weak derivatives through strong L2 limits. This closes the nonlinear H2 calculation after its explicit product limits.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_weak_derivative_limit line 22

theorem OAI.PositiveEinsteinFour.Geometry.scalar_H2_of_strong_jets line 36

Source documentation

Strong convergence of the two jets supplies H2 for their value limit.

theorem scalar_H2_of_strong_jets (f : ℕ → L2) (G : Fin 4 → ℕ → L2)
    (H : Fin 4 → Fin 4 → ℕ → L2) (u : L2) (g : Fin 4 → L2) (h : Fin 4 → Fin 4 → L2)
    (hf : Tendsto f atTop (𝓝 u))
    (hg : ∀ i, Tendsto (G i) atTop (𝓝 (g i)))
    (hh : ∀ i j, Tendsto (H i j) atTop (𝓝 (h i j)))
    (hD : ∀ n i, scalarCoordinateDerivative i (f n : T) = (G i n : T))
    (hDD : ∀ n i j, scalarCoordinateDerivative i (G j n : T) = (H i j n : T)) :
    MemSobolev 2 2 (u : T) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative