ScalarH1CompositionL2.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded scalar multipliers on real L², including convergence when the multiplier converges almost everywhere and the multiplied vector converges strongly. This is the analytic closure step in the scalar H¹ chain rule.

def OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply line 20
theorem OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply_coe line 27
theorem OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply_norm_le line 32
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_norm_sq line 40

theorem OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply_tendsto_fixed line 47

Source documentation

Almost-everywhere convergence of uniformly bounded multipliers is strong on each fixed L² vector.

theorem scalarCompositionL2Multiply_tendsto_fixed {a : ℕ → X → ℝ} {b : X → ℝ}
    (ha : ∀ n, AEStronglyMeasurable (a n) μ) (hb : AEStronglyMeasurable b μ)
    {C : ℝ} (hC : 0 ≤ C) (haC : ∀ n x, |a n x| ≤ C) (hbC : ∀ x, |b x| ≤ C)
    (hab : ∀ᵐ x ∂μ, Tendsto (fun n => a n x) atTop (𝓝 (b x)))
    (f : Lp ℝ 2 μ) :
    Tendsto (fun n => scalarCompositionL2Multiply (a n) (ha n) (haC n) f) atTop
      (𝓝 (scalarCompositionL2Multiply b hb hbC f)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply

theorem OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply_tendsto line 93

Source documentation

Both factors may move: bounded multiplier convergence and strong L² convergence imply strong convergence of their product.

theorem scalarCompositionL2Multiply_tendsto {a : ℕ → X → ℝ} {b : X → ℝ}
    (ha : ∀ n, AEStronglyMeasurable (a n) μ) (hb : AEStronglyMeasurable b μ)
    {C : ℝ} (hC : 0 ≤ C) (haC : ∀ n x, |a n x| ≤ C) (hbC : ∀ x, |b x| ≤ C)
    (hab : ∀ᵐ x ∂μ, Tendsto (fun n => a n x) atTop (𝓝 (b x)))
    {f : ℕ → Lp ℝ 2 μ} {g : Lp ℝ 2 μ} (hfg : Tendsto f atTop (𝓝 g)) :
    Tendsto (fun n => scalarCompositionL2Multiply (a n) (ha n) (haC n) (f n)) atTop
      (𝓝 (scalarCompositionL2Multiply b hb hbC g)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCompositionL2Multiply