RegularBochnerForm.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polarized Bochner forms on a finite regular span

def OAI.RegularPointCoordinates.regularBochnerForm line 20

Source documentation

The full weak Bochner form retains both L² source terms.

def regularBochnerForm (K : ℝ)
    (U : Euclidean m →L[ℝ] SobolevSpace μ hQ) (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace μ hQ)
    (q : X →ᵇ ℝ) (ψ : SobolevSpace μ hQ) (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ (U a) x≤L a) :
    Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ :=
…

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

theorem OAI.RegularPointCoordinates.regularBochnerForm_symmetric line 53