ScalarL2Order

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

Internal scalar L² order identities

This module collects elementary scalar L² identities used by the divergence-form comparison and positivity arguments.

theorem DivergenceFormProcess.Form.Internal.scalarL2_inner_nonneg_of_ae_nonneg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f g : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) (hg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑g x) : 0 ≤ inner ℝ f g

The scalar L² inner product of almost-everywhere nonnegative functions is nonnegative.

theorem DivergenceFormProcess.Form.Internal.scalarL2_inner_sub_nonpos_of_ae_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f g p : ↥(HCPolySupport.ScalarL2 U)) (hfg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑f x ≤ ↑↑g x) (hp : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑p x) : inner ℝ (f - g) p ≤ 0

Ordered scalar L² functions have nonpositive difference pairing against an almost-everywhere nonnegative function.

theorem DivergenceFormProcess.Form.Internal.scalarL2_inner_eq_self_of_ae_eq_max {d : ℕ} {U : Set (HCPolySupport.Vec d)} (z p : ↥(HCPolySupport.ScalarL2 U)) (hp : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑p x = max (↑↑z x) 0) : inner ℝ z p = inner ℝ p p

Pairing with the positive part equals the positive part's self-pairing.

theorem DivergenceFormProcess.Form.Internal.scalarL2_inner_eq_neg_self_of_ae_eq_max_neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u v : ↥(HCPolySupport.ScalarL2 U)) (hv : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑v x = max (-↑↑u x) 0) : inner ℝ u v = -inner ℝ v v

Pairing with the negative part is the negative of that part's self-pairing.