RegularBochnerMeasure.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common full Bochner measure for a finite regular span

theorem OAI.RegularPointCoordinates.coordinateBilinear_of_form line 17

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_span_bochner_sobolev_measure line 31

Source documentation

The scalar RCD Bochner measures polarize to one positive bilinear measure on the whole regular span. No source derivatives are assumed.

theorem NoncollapsedRCD.regular_span_bochner_sobolev_measure {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {r : ℝ} (hr : 0<r)
    (U : Euclidean m →L[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (D : Euclidean m →L[ℝ] Lp ℝ 2 (hausdorff n X))
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂hausdorff n X, SobolevSpace.minimalSlope (hausdorff n X) hX.quadratic (U a) x≤L a)
    (hcompact : ∀ a, ∃ (v : X → ℝ) (Q : ℝ≥0), LipschitzWith Q v ∧ HasCompactSupport v ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic (U a) =ᵐ[hausdorff n X] v)
    (hD : ∀ a, IsWeakLaplacian (hausdorff n X) hX.quadratic (U a) (D a))
    (hH : ∀ a, SobolevSpace.toLp (hausdorff n X) hX.quadratic (H a a) =ᵐ[hausdorff n X]
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_span_bochner_measure line 132

Source documentation

The compact Lipschitz test specialization of the full Sobolev test identity.

theorem NoncollapsedRCD.regular_span_bochner_measure {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {r : ℝ} (hr : 0<r)
    (U : Euclidean m →L[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (D : Euclidean m →L[ℝ] Lp ℝ 2 (hausdorff n X))
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace (hausdorff n X) hX.quadratic)
    (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂hausdorff n X, SobolevSpace.minimalSlope (hausdorff n X) hX.quadratic (U a) x≤L a)
    (hcompact : ∀ a, ∃ (v : X → ℝ) (Q : ℝ≥0), LipschitzWith Q v ∧ HasCompactSupport v ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic (U a) =ᵐ[hausdorff n X] v)
    (hD : ∀ a, IsWeakLaplacian (hausdorff n X) hX.quadratic (U a) (D a))
    (hH : ∀ a, SobolevSpace.toLp (hausdorff n X) hX.quadratic (H a a) =ᵐ[hausdorff n X]
…