WeakTesting #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Weak testing for the small-contrast harmonic comparison #
This file supplies the measure-theoretic part of e.harmapprox.Schauder.
The public chain uses coefficient measurability and the a.e. operator-norm
distance directly.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integrableOn_vecNormSq_of_memVectorL2
{d : ℕ}
{W : Set (HCPolySupport.Vec d)}
{F : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hF : HCPolySupport.MemVectorL2 W F)
:
MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (F x)) W MeasureTheory.volume
Squared Euclidean magnitude is integrable for a vector L² field.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.abs_integral_vecDot_le_sqrt_energy_mul_sqrt_energy
{d : ℕ}
{W : Set (HCPolySupport.Vec d)}
{F G : HCPolySupport.Vec d → HCPolySupport.Vec d}
[MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn W)]
(hF : HCPolySupport.MemVectorL2 W F)
(hG : HCPolySupport.MemVectorL2 W G)
:
|∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (F x) (G x)| ≤ √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (F x)) * √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (G x))
Euclidean Cauchy--Schwarz for two vector L² fields, expressed in the
square-energy language used by the harmonic comparison.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integral_vecNormSq_coefficientSubIdentity_mul_le_of_measurable
{d : ℕ}
{W : Set (HCPolySupport.Vec d)}
{a : HCPolySupport.CoeffField d}
{H : HCPolySupport.Vec d → HCPolySupport.Vec d}
{delta : ℝ}
(hmeas : Measurable a)
(ha : CoefficientIdentityDistanceLE W a delta)
(hH : HCPolySupport.MemVectorL2 W H)
:
∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (HCPolySupport.matVecMul (a x - 1) (H x)) ≤ delta ^ 2 * ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (H x)
Measurable-coefficient form of the perturbation-field estimate.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_integral_vecNormSq_coefficientSubIdentity_mul_le_of_measurable
{d : ℕ}
{W : Set (HCPolySupport.Vec d)}
{a : HCPolySupport.CoeffField d}
{H : HCPolySupport.Vec d → HCPolySupport.Vec d}
{delta : ℝ}
(hmeas : Measurable a)
(ha : CoefficientIdentityDistanceLE W a delta)
(hdelta : 0 ≤ delta)
(hH : HCPolySupport.MemVectorL2 W H)
:
√(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (HCPolySupport.matVecMul (a x - 1) (H x))) ≤ delta * √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (H x))
Square-root measurable-coefficient form of the perturbation estimate.