Coarse-graining support: Support.Sobolev.Foundations.MeanZero

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

noncomputable def HCPolySupport.integralAverage {d : ℕ} (U : Set (Vec d)) (u : Vec d → ℝ) : ℝ

The integral of u over U multiplied by the reciprocal of the real volume of U.

Equations

• HCPolySupport.integralAverage U u = (MeasureTheory.volume U).toReal⁻¹ * ∫ (x : HCPolySupport.Vec d) in U, u x

theorem HCPolySupport.H1Function.integrableOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : MeasureTheory.IntegrableOn u.toFun U MeasureTheory.volume

noncomputable def HCPolySupport.H1Function.const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (c : ℝ) : H1Function U

The constant H¹ function with value c and zero weak gradient.

Equations

• HCPolySupport.H1Function.const c = { toFun := fun (x : HCPolySupport.Vec d) => c, grad := fun (x : HCPolySupport.Vec d) => 0, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

@[simp]

theorem HCPolySupport.H1Function.const_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (c : ℝ) (x : Vec d) : (const c).toFun x = c

@[simp]

theorem HCPolySupport.H1Function.grad_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (c : ℝ) (x : Vec d) : (const c).grad x = 0

noncomputable def HCPolySupport.H1Function.addConst {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (c : ℝ) : H1Function U

The H¹ function u + c, retaining the weak gradient of u.

Equations

• u.addConst c = u + HCPolySupport.H1Function.const c

@[simp]

theorem HCPolySupport.H1Function.addConst_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (c : ℝ) (x : Vec d) : (u.addConst c).toFun x = u.toFun x + c

@[simp]

theorem HCPolySupport.H1Function.grad_addConst {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (c : ℝ) (x : Vec d) : (u.addConst c).grad x = u.grad x

noncomputable def HCPolySupport.H1Function.subAverage {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : H1Function U

The H¹ function obtained by subtracting its integral average on U.

Equations

• u.subAverage = u.addConst (-HCPolySupport.integralAverage U u.toFun)

@[simp]

theorem HCPolySupport.H1Function.subAverage_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (x : Vec d) : u.subAverage.toFun x = u.toFun x - integralAverage U u.toFun

@[simp]

theorem HCPolySupport.H1Function.grad_subAverage {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (x : Vec d) : u.subAverage.grad x = u.grad x

theorem HCPolySupport.H1Function.meanZeroOn_subAverage {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : MeanZeroOn U u.subAverage.toFun

noncomputable def HCPolySupport.H1Function.coordOnIsBoundedDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hBounded : IsBoundedDomain U) (i : Fin d) : H1Function U

The coordinate function x ↦ x i as an H¹ function on a bounded measurable domain, with gradient eᵢ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H1Function.coordOnIsBoundedDomain_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hBounded : IsBoundedDomain U) (i : Fin d) (x : Vec d) : (coordOnIsBoundedDomain hU hBounded i).toFun x = x i

@[simp]

theorem HCPolySupport.H1Function.coordOnIsBoundedDomain_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hBounded : IsBoundedDomain U) (i : Fin d) (x : Vec d) : (coordOnIsBoundedDomain hU hBounded i).grad x = basisVec i

noncomputable def HCPolySupport.H1Function.coordOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (i : Fin d) : H1Function U

The coordinate function x ↦ x i as an H¹ function on a Sobolev regular domain, with gradient eᵢ.

Equations

• HCPolySupport.H1Function.coordOnIsSobolevRegularDomain hU i = HCPolySupport.H1Function.coordOnIsBoundedDomain ⋯ ⋯ i

@[simp]

theorem HCPolySupport.H1Function.coordOnIsSobolevRegularDomain_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (i : Fin d) (x : Vec d) : (coordOnIsSobolevRegularDomain hU i).toFun x = x i

@[simp]

theorem HCPolySupport.H1Function.coordOnIsSobolevRegularDomain_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (i : Fin d) (x : Vec d) : (coordOnIsSobolevRegularDomain hU i).grad x = basisVec i

noncomputable def HCPolySupport.H1Function.averageGradient {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : Vec d

The componentwise average gradient of an H¹ function on a finite-measure domain.

Equations

• u.averageGradient i = HCPolySupport.integralAverage U fun (x : HCPolySupport.Vec d) => u.grad x i

theorem HCPolySupport.H1Function.averageGradient_eq_zero_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hzero : (fun (i : Fin d) => ∫ (x : Vec d) in U, u.grad x i) = 0) : u.averageGradient = 0

If each gradient coordinate of an H¹ function has zero integral, then its componentwise average gradient vanishes.

noncomputable def HCPolySupport.H1Function.affineOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (p : Vec d) : H1Function U

The affine H¹ function on a Sobolev-regular domain with constant gradient p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H1Function.affineOnIsSobolevRegularDomain_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (p x : Vec d) : (affineOnIsSobolevRegularDomain hU p).toFun x = ∑ i : Fin d, p i * x i

@[simp]

theorem HCPolySupport.H1Function.affineOnIsSobolevRegularDomain_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (p x : Vec d) : (affineOnIsSobolevRegularDomain hU p).grad x = p

noncomputable def HCPolySupport.H1Function.averageGradientAffineOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (u : H1Function U) : H1Function U

The affine H¹ function with gradient equal to u.averageGradient.

Equations

• HCPolySupport.H1Function.averageGradientAffineOnIsSobolevRegularDomain hU u = HCPolySupport.H1Function.affineOnIsSobolevRegularDomain hU u.averageGradient

@[simp]

theorem HCPolySupport.H1Function.averageGradientAffineOnIsSobolevRegularDomain_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (u : H1Function U) (x : Vec d) : (averageGradientAffineOnIsSobolevRegularDomain hU u).grad x = u.averageGradient

@[simp]

theorem HCPolySupport.H1Function.sub_averageGradientAffineOnIsSobolevRegularDomain_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (u : H1Function U) (x : Vec d) : (u - averageGradientAffineOnIsSobolevRegularDomain hU u).grad x = u.grad x - u.averageGradient

theorem HCPolySupport.H1Function.exists_h1_sub_averageGradient_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) (u : H1Function U) : ∃ (w : H1Function U), w.grad = fun (x : Vec d) => u.grad x - u.averageGradient

Honest H¹ affine decomposition: subtracting the affine function with gradient averageGradient leaves an H¹ function whose gradient has zero average.

theorem HCPolySupport.H1Function.integral_eq_zero_of_averageGradient_eq_zero {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (havg : u.averageGradient = 0) : (fun (i : Fin d) => ∫ (x : Vec d) in U, u.grad x i) = 0

If the average gradient vanishes and the domain has nonzero volume, then the componentwise gradient integrals vanish.