BoundedSplittingCoordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

First-order splitting data are local to their representatives

theorem OAI.RegularPointCoordinates.localGamma_pair_congr_ae line 17

Source documentation

Local equality in both slots preserves the actual gradient pairing.

theorem localGamma_pair_congr_ae {Ω : Set X} {f f' g g' : SobolevSpace μ hQ}
    (hf : SobolevSpace.toLp μ hQ f' =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ f)
    (hg : SobolevSpace.toLp μ hQ g' =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g) :
    localGamma μ hQ f' g' =ᵐ[μ.restrict Ω] localGamma μ hQ f g := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.congr_representative line 30
Source documentation
Changing global Sobolev extensions preserves every first-order splitting condition when the local pointwise coordinate representative is unchanged.
```
theorem FirstOrderSplittingOn.congr_representative {n : ℕ} {p : X} {r ε : ℝ}
    {u u' : Fin n → SobolevSpace μ hQ} {v : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p r ε u v)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u' j) =ᵐ[μ.restrict (ball p r)] fun x => v x j) :
    FirstOrderSplittingOn μ hQ p r ε u' v := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.SobolevSpace.toLp

theorem OAI.RegularPointCoordinates.bounded_normalized_splitting line 53

Source documentation

A centered metric approximation supplies globally bounded extensions of the SAME local splitting map; no global boundedness input is required.

theorem bounded_normalized_splitting {n : ℕ} {p : X} {r ε : ℝ}
    (hr : 0 < r) (hε : 0 ≤ ε) (hε1 : ε ≤ 1)
    (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n)
    (hfirst : FirstOrderSplittingOn μ hQ p (4 * r) ε u v) (hv : v p = 0)
    (hmetric : IsPointedApproximation p 0 r 4 ε (fun x => r⁻¹ • v x)) :
    ∃ u' : Fin n → SobolevSpace μ hQ,
      (∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u' j) x| ≤ 5 * r) ∧
      FirstOrderSplittingOn μ hQ p (4 * r) ε u' v := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.SobolevSpace.toLp