OAI/Geometry/RCD/Sobolev/CompactTestPairing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.compactTestBound line 17
2. theorem OAI.RegularPointCoordinates.compactTestBound_nonneg line 20
3. theorem OAI.RegularPointCoordinates.compactTestBound_spec line 23
4. def OAI.RegularPointCoordinates.compactTestLp line 28
5. theorem OAI.RegularPointCoordinates.compactTestLp_coe line 38
6. theorem OAI.RegularPointCoordinates.compactTestLp_normalized_norm line 45
7. theorem OAI.RegularPointCoordinates.compactTest_one_pairing line 55
8. theorem OAI.RegularPointCoordinates.compactTest_sobolev_pairing line 72
9. theorem OAI.RegularPointCoordinates.normalized_euler_identity line 83

   Source documentation

   Normalization preserves the full finite affine Euler identity.

   theorem normalized_euler_identity {n : ℕ} (s : Set X) (hfin : μ s ≠ ∞)
       (w e d one : Lp ℝ 2 (μ.restrict s)) (u : Fin n → Lp ℝ 2 (μ.restrict s))
       (ell : Fin n → ℝ) (k a : ℝ)
       (hid : a • d = w + ∑ j, ell j • u j + k • one + e) :
       a • normalizeLocalL2 μ s hfin d = normalizeLocalL2 μ s hfin w +
         ∑ j, ell j • normalizeLocalL2 μ s hfin (u j) +
           k • normalizeLocalL2 μ s hfin one + normalizeLocalL2 μ s hfin e := by
   …

   Mentions: OAI.RegularPointCoordinates.normalizeLocalL2

10. theorem OAI.RegularPointCoordinates.compactTest_radial_pairing line 96

    Source documentation

    The normalized radial pairing is exactly the rescaled test integral appearing in Ambrosio--Honda's weak gradient convergence.

    theorem compactTest_radial_pairing {n : ℕ} (s : Set X) (hfin : μ s ≠ ∞)
        (V : X → Euclidean n) (hV : Measurable V) (ψ : Euclidean n → ℝ)
        (hc : Continuous ψ) (hs : HasCompactSupport ψ) (f w : SobolevSpace μ hQ)
        {B : ℝ} (hf : ∀ᵐ x ∂μ.restrict s, localGamma μ hQ f f x ≤ B) (a : ℝ) :
        ⟪normalizeLocalL2 μ s hfin (compactTestLp μ s hfin V hV ψ hc hs),
          a • normalizeLocalL2 μ s hfin (localRadialDerivative μ hQ s f hf w)⟫_ℝ =
            (μ.real s)⁻¹ * ∫ x in s, ψ (V x) * (a * localGamma μ hQ f w x) ∂μ := by
    …

    Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.compactTestLp, OAI.RegularPointCoordinates.localRadialDerivative