BochnerGramSource.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Integrating the full sources in the Gram product equation

def OAI.RegularPointCoordinates.bochnerGramSource line 19
Source documentation
Full source of a Gram entry with its Bochner measure separated out.
```
def bochnerGramSource (K : ℝ) (f g df dg : SobolevSpace μ hQ)
    (S : SignedMeasure X) : SignedMeasure X :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.integral_bochnerGramSource line 24
theorem OAI.RegularPointCoordinates.integral_cutoffMeasureSource line 35

theorem OAI.RegularPointCoordinates.integral_cutoffMeasureSource_local line 48

Source documentation

A compactly supported test sees only the local L² source.

theorem integral_cutoffMeasureSource_local {Ω : Set X} (hΩ : MeasurableSet Ω)
    (g c : SobolevSpace μ hQ) (d e : Lp ℝ 2 μ) (ν : SignedMeasure X)
    (χ q : X →ᵇ ℝ) (hqs : tsupport q ⊆ Ω) (hde : d =ᵐ[μ.restrict Ω] e) :
    signedTestIntegral q (cutoffMeasureSource μ hQ g c d ν χ) =
      signedTestIntegral q (cutoffMeasureSource μ hQ g c e ν χ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.signedTestIntegral, OAI.RegularPointCoordinates.cutoffMeasureSource

theorem OAI.RegularPointCoordinates.integral_gramProductSource line 66

Source documentation

The two full product sources combine to the integrable drift density. The Bochner parts keep their actual signed measures.

theorem integral_gramProductSource (K : ℝ)
    (f g h df dg dh Fg Fh : SobolevSpace μ hQ)
    (Sg Sh : SignedMeasure X) (G H q : X →ᵇ ℝ)
    (hG : SobolevSpace.toLp μ hQ g =ᵐ[μ] G)
    (hH : SobolevSpace.toLp μ hQ h =ᵐ[μ] H) :
    signedTestIntegral q
      (cutoffMeasureSource μ hQ Fh g (SobolevSpace.toLp μ hQ dg)
        (bochnerGramSource μ hQ K f h df dh Sh) G+
      cutoffMeasureSource μ hQ Fg h (SobolevSpace.toLp μ hQ dh)
        (bochnerGramSource μ hQ K f g df dg Sg) H) =
      2*signedTestIntegral (q*G) Sh+2*signedTestIntegral (q*H) Sg+
        (∫ x, q x*bochnerProductDensity μ hQ K f g h df dg dh Fg Fh x ∂μ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.signedTestIntegral, OAI.RegularPointCoordinates.cutoffMeasureSource, OAI.RegularPointCoordinates.bochnerGramSource, OAI.RegularPointCoordinates.bochnerProductDensity