NormalizedEnergy

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

Normalized Euclidean energy calculus for the small-contrast iteration

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedL2On_coord_le_vectorNormalizedL2On {d : ℕ} {W : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 W F) (i : Fin d) : (Section4.Support.normalizedL2On W fun (x : HCPolySupport.Vec d) => F x i) ≤ vectorNormalizedL2On W F

One coordinate is controlled by the normalized energy of any square-integrable vector field. No measurability, volume or positivity assumption on the domain is needed.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_eq_toReal_eLpNorm_div {d : ℕ} {W : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 W F) : vectorNormalizedL2On W F = (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (F x)) 2 (MeasureTheory.volume.restrict W)).toReal / √(MeasureTheory.volume W).toReal

Dictionary from the vector normalized energy to the Hilbert realization's ordinary L² norm.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_integral_vecNormSq_eq_sqrt_volume_mul_vectorNormalizedL2On {d : ℕ} {W : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hW : 0 < (MeasureTheory.volume W).toReal) (hF : HCPolySupport.MemVectorL2 W F) : √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (F x)) = √(MeasureTheory.volume W).toReal * vectorNormalizedL2On W F

Raw and normalized Euclidean energies differ by the square root of the window volume.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_add_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {F G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 W F) (hG : HCPolySupport.MemVectorL2 W G) : (vectorNormalizedL2On W fun (x : HCPolySupport.Vec d) => F x + G x) ≤ vectorNormalizedL2On W F + vectorNormalizedL2On W G

Minkowski for normalized Euclidean vector energy.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_sub_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {F G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 W F) (hG : HCPolySupport.MemVectorL2 W G) : (vectorNormalizedL2On W fun (x : HCPolySupport.Vec d) => F x - G x) ≤ vectorNormalizedL2On W F + vectorNormalizedL2On W G

Triangle inequality in subtraction form.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_le_of_subset {d : ℕ} {W W' : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hsub : W' ⊆ W) (hWpos : 0 < (MeasureTheory.volume W).toReal) (hW'pos : 0 < (MeasureTheory.volume W').toReal) (hf : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => HCPolySupport.HilbertVec.ofVec (f x)) 2 (MeasureTheory.volume.restrict W)) : vectorNormalizedL2On W' f ≤ √((MeasureTheory.volume W).toReal / (MeasureTheory.volume W').toReal) * vectorNormalizedL2On W f

Restriction of the normalized Euclidean vector L2 carrier.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_ratio_half_euclideanBall {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall z (r / 2))).toReal = 2 ^ d

The exact volume ratio between a ball and its half-radius subball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_volume_ratio_half_euclideanBall {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : √((MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall z (r / 2))).toReal) = (1 / 2) ^ (-↑d / 2)

Square-root form of the half-ball volume ratio.