FirstOrderLocalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting harmonic splitting data to nearby balls

theorem OAI.RegularPointCoordinates.dirichlet_mono line 18
theorem OAI.RegularPointCoordinates.IsSobolevHarmonicOn.mono line 25

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.restrict_ball line 34

Source documentation

First-order splitting conditions localize with exactly the volume-ratio loss in the averaged Gram error. Harmonicity and representatives are genuine restrictions of the same original functions.

theorem FirstOrderSplittingOn.restrict_ball {n : ℕ} {p q : X} {R r ε C : ℝ}
    {u : Fin n → SobolevSpace μ hQ} {v : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p R ε u v)
    (hsub : ball q r ⊆ ball p R) (hε : 0 ≤ ε) (hC : 1 ≤ C)
    (hszero : μ (ball q r) ≠ 0) (hsfin : μ (ball q r) ≠ ∞)
    (htzero : μ (ball p R) ≠ 0) (htfin : μ (ball p R) ≠ ∞)
    (hvol : μ.real (ball p R) ≤ C * μ.real (ball q r)) :
    FirstOrderSplittingOn μ hQ q r (C * ε) u v := by
…

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