BoundedSquareVariation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar differentiation of a bounded L² square against a varying weight

theorem OAI.RegularPointCoordinates.inner_boundedLpSquare line 18
Source documentation
Pairing a bounded L² square with a bounded weight agrees with the continuous weighted quadratic form.
```
theorem inner_boundedLpSquare (f w : Lp ℝ 2 μ) (V : Lp ℝ ∞ μ)
    (hV : V =ᵐ[μ] w) (C : ℝ) (hC : 0 ≤ C) (hf : ∀ᵐ x ∂μ, |f x| ≤ C) :
    inner ℝ w (boundedLpSquare μ f C hC hf) = inner ℝ f (lpMultiplier μ V f) := by
…
```
Mentions: OAI.RegularPointCoordinates.boundedLpSquare, OAI.RegularPointCoordinates.lpMultiplier

theorem OAI.RegularPointCoordinates.boundedSquare_pairing_hasDerivAt line 29

Source documentation

The derivative uses only L² derivatives of the two paths; boundedness supplies the extra continuity required for the square.

theorem boundedSquare_pairing_hasDerivAt {F W : ℝ → Lp ℝ 2 μ} {t C : ℝ}
    {F' W' : Lp ℝ 2 μ} (hC : 0 ≤ C) (hb : ∀ s, ∀ᵐ x ∂μ, |F s x| ≤ C)
    (hF : HasDerivAt F F' t) (hW : HasDerivAt W W' t)
    (V : Lp ℝ ∞ μ) (hV : V =ᵐ[μ] W t) :
    HasDerivAt (fun s => inner ℝ (W s) (boundedLpSquare μ (F s) C hC (hb s)))
      (inner ℝ W' (boundedLpSquare μ (F t) C hC (hb t))+
        2*inner ℝ F' (lpMultiplier μ V (F t))) t := by
…

Mentions: OAI.RegularPointCoordinates.boundedLpSquare, OAI.RegularPointCoordinates.lpMultiplier