Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch01.Theorems.MeanSquareDeviation

Coarse-graining support: Support.Book.Ch01.Theorems.MeanSquareDeviation #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Mean-square deviation toolkit #

Scalar and vector mean-square deviation of a field from a constant, together with the companion mean-square oscillation, are the L²-normalized quantities used to measure how far a field sits from its average on a domain. This file collects their basic identities: rewriting the vector deviation as a volume average of the squared coordinate norm of the centered field (for square- integrable fields), the explicit-Euclidean-ball finiteness facts they rely on, and the norm-equivalence bound of the deviation from zero by the ambient L² seminorm.

source
noncomputable def HCPolySupport.Book.Ch01.meanSquareDeviationOn {d : ℕ} (V : Set (Vec d)) (u : Vec d → ℝ) (c : ℝ) :
ℝ

Mean square deviation of a scalar function from a constant on a set.

Equations
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch01.euclideanUnitBallVolume (d : ℕ) :
    ℝ

    Real volume of the explicit unit Euclidean ball.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.Book.Ch01.meanSquareDeviationVecOn {d : ℕ} (V : Set (Vec d)) (h : Vec d → Vec d) (c : Vec d) :
      ℝ

      Componentwise mean square deviation of a vector field from a constant.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.Book.Ch01.meanSquareOscillationVecOn {d : ℕ} (V : Set (Vec d)) (h : Vec d → Vec d) :
        ℝ

        Componentwise mean square oscillation of a vector field on a set.

        Equations
        Instances For
          source
          theorem HCPolySupport.Book.Ch01.meanSquareDeviationVecOn_eq_volumeAverage_vecNormSq_sub {d : ℕ} {V : Set (Vec d)} {h : Vec d → Vec d} {c : Vec d} (hint : ∀ (k : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (h x k - c k) ^ 2) V MeasureTheory.volume) :
          meanSquareDeviationVecOn V h c = volumeAverage V fun (x : Vec d) => vecNormSq (h x - c)

          Vector mean-square deviation is the volume average of the squared coordinate norm of the centered vector field, when the componentwise squares are integrable.

          source
          theorem HCPolySupport.Book.Ch01.integrableOn_coord_sub_const_sq_of_memVectorL2 {d : ℕ} {V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn V)] {h : Vec d → Vec d} (hh : MemVectorL2 V h) (c : Vec d) (k : Fin d) :
          MeasureTheory.IntegrableOn (fun (x : Vec d) => (h x k - c k) ^ 2) V MeasureTheory.volume

          For an L² vector field on a finite-measure set, every coordinate after subtracting a constant has an integrable square.

          source
          theorem HCPolySupport.Book.Ch01.meanSquareDeviationVecOn_eq_volumeAverage_vecNormSq_sub_of_memVectorL2 {d : ℕ} {V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn V)] {h : Vec d → Vec d} (hh : MemVectorL2 V h) (c : Vec d) :
          meanSquareDeviationVecOn V h c = volumeAverage V fun (x : Vec d) => vecNormSq (h x - c)

          Vector mean-square deviation is the volume average of the squared coordinate norm of the centered vector field for every L² vector field on a finite-measure set.

          source
          theorem HCPolySupport.Book.Ch01.volume_euclideanBall_ne_top {d : ℕ} (x : Vec d) (r : ℝ) :
          MeasureTheory.volume (euclideanBall x r) ≠ ⊤

          Explicit Euclidean balls have finite volume.

          source
          theorem HCPolySupport.Book.Ch01.volume_euclideanBall_toReal_ne_zero {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) :
          (MeasureTheory.volume (euclideanBall x r)).toReal ≠ 0

          Positive-radius explicit Euclidean balls have nonzero real volume.

          source
          theorem HCPolySupport.Book.Ch01.isFiniteMeasure_volumeMeasureOn_euclideanBall {d : ℕ} (x : Vec d) (r : ℝ) :
          MeasureTheory.IsFiniteMeasure (volumeMeasureOn (euclideanBall x r))

          The volume measure restricted to an explicit Euclidean ball is finite.

          source
          theorem HCPolySupport.Book.Ch01.meanSquareDeviationVecOn_zero_le_card_mul_volume_inv_mul_eLpNorm_sq {d : ℕ} {V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn V)] {F : Vec d → Vec d} (hvol : 0 < (MeasureTheory.volume V).toReal) (hF : MemVectorL2 V F) :
          meanSquareDeviationVecOn V F 0 ≤ ↑(Fintype.card (Fin d)) * (MeasureTheory.volume V).toReal⁻¹ * (MeasureTheory.eLpNorm F 2 (volumeMeasureOn V)).toReal ^ 2

          Mean-square deviation from zero is controlled by the square of the ambient L² seminorm, with the expected finite-dimensional norm-equivalence factor.