CovectorCoefficientRecovery.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Two-center coefficient recovery from the actual affine L2 residual

theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.covector_coefficient_recovery line 19

Source documentation

Published harmonic gradient control and exact normalization recover the difference B of the radial matrices from the affine commutator residual. The displayed residual is the output of the Sobolev commutator identity.

theorem LocalHarmonicL2GradientInput.covector_coefficient_recovery
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
        (N : Euclidean n ≃L[ℝ] Euclidean n),
      IsExactMeanNormalization (hausdorff n X) hX.quadratic
        (sobolevColumnMap (hausdorff n X) hX.quadratic u)
        (ball p (R / 2)) measurableSet_ball N →
      (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) (u j)) →
      ∀ η : SobolevSpace (hausdorff n X) hX.quadratic,
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.IsSobolevHarmonicOn