OAI/Geometry/RCD/Sobolev/BochnerMeasurePolarization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full off-diagonal Bochner test identity

  1. theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.polarized_test line 19

    Source documentation

    Diagonal identities determine the integral of every off-diagonal signed measure, with no absolute-continuity assumption.

    theorem PositiveBilinearMeasure.polarized_test (M : PositiveBilinearMeasure X E)
    (q : X →ᵇ ℝ) (B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ)
    (hB : ∀ a b, B a b=B b a)
    (h : ∀ a, (∫ x, q x ∂M.measure a)=B a a) (a b : E) :
    signedTestIntegral q (M.bilinear a b)=B a b := by
…

    Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.signedTestIntegral