RegularCoreBochner.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full Bochner measures constructed for the regular test algebra

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_bochner_sobolev_measure line 17
Source documentation
A finite collection of actual regular tests determines a single positive bilinear Bochner measure, with the exact weak test identity.
```
theorem NoncollapsedRCD.regular_core_bochner_sobolev_measure {K : ℝ} {n m : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {Ω : Set X} (u : Fin m → compactLaplacianCore (hausdorff n X) hX.quadratic Ω)
    {r : ℝ} (hr : 0<r) :
    let U := sobolevColumnMap (hausdorff n X) hX.quadratic (fun i => (u i).val)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.sobolevColumnMap
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_bochner_measure line 44
Source documentation
The Lipschitz test specialization, preserving the original interface.
```
theorem NoncollapsedRCD.regular_core_bochner_measure {K : ℝ} {n m : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {Ω : Set X} (u : Fin m → compactLaplacianCore (hausdorff n X) hX.quadratic Ω)
    {r : ℝ} (hr : 0<r) :
    let U := sobolevColumnMap (hausdorff n X) hX.quadratic (fun i => (u i).val)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.sobolevColumnMap