Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.DivergenceForm.CoefficientPairing

CoefficientPairing #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Coefficient pairing #

This file defines the integral pairing induced by a coefficient field on Hilbert-vector L² fields. It also proves the pairing signs obtained when the second field agrees almost everywhere with an indicator localization of the first field or its negative.

Main definitions #

Main results #

source
noncomputable def DivergenceFormProcess.Form.coefficientPairing {d : ℕ} (a : HCPolySupport.CoeffField d) (U : Set (HCPolySupport.Vec d)) (F G : ↥(HCPolySupport.HilbertVectorL2 U)) :
ℝ

The integral pairing of two Hilbert-vector L² fields induced by a coefficient field.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem DivergenceFormProcess.Form.coefficientPairing_nonneg_of_ae_eq_indicator {d : ℕ} {lam Lam : ℝ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (F G : ↥(HCPolySupport.HilbertVectorL2 U)) (S : Set (HCPolySupport.Vec d)) (hG : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑G x = S.indicator (↑↑F) x) :
    0 ≤ coefficientPairing a U F G

    The coefficient pairing is nonnegative when its second field agrees almost everywhere with an indicator localization of its first field. The set is arbitrary; its indicator is controlled through the supplied almost-everywhere identity.

    source
    theorem DivergenceFormProcess.Form.coefficientPairing_nonpos_of_ae_eq_neg_indicator {d : ℕ} {lam Lam : ℝ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (F G : ↥(HCPolySupport.HilbertVectorL2 U)) (S : Set (HCPolySupport.Vec d)) (hG : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑G x = S.indicator (fun (y : HCPolySupport.Vec d) => -↑↑F y) x) :
    coefficientPairing a U F G ≤ 0

    The coefficient pairing is nonpositive when its second field agrees almost everywhere with an indicator localization of the negative of its first field. The set is arbitrary; its indicator is controlled through the supplied almost-everywhere identity.