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

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

noncomputable def HCPolySupport.H1MeanZeroFunction.translate {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) (z : Vec d) : H1MeanZeroFunction (translateSet z U)

Translate a mean-zero H¹(U) witness to H¹(U + z).

Equations

• u.translate z = { toH1Function := u.toH1Function.translate z, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.translate_toH1Function {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) (z : Vec d) : (u.translate z).toH1Function = u.toH1Function.translate z

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.translate_apply {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) (z x : Vec d) : (u.translate z).toH1Function.toFun x = u.toH1Function.toFun (x - z)

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.translate_grad {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) (z x : Vec d) : (u.translate z).toH1Function.grad x = u.toH1Function.grad (x - z)

noncomputable def HCPolySupport.H1MeanZeroFunction.untranslate {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) : H1MeanZeroFunction U

Pull a mean-zero H¹(U + z) witness back to H¹(U).

Equations

• HCPolySupport.H1MeanZeroFunction.untranslate z u = { toH1Function := HCPolySupport.H1Function.untranslate z u.toH1Function, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.untranslate_toH1Function {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) : (untranslate z u).toH1Function = H1Function.untranslate z u.toH1Function

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.untranslate_apply {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) (x : Vec d) : (untranslate z u).toH1Function.toFun x = u.toH1Function.toFun (x + z)

@[simp]

theorem HCPolySupport.H1MeanZeroFunction.untranslate_grad {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) (x : Vec d) : (untranslate z u).toH1Function.grad x = u.toH1Function.grad (x + z)

theorem HCPolySupport.H1MeanZeroFunction.valueL2Norm_untranslate_eq {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) : (untranslate z u).valueL2Norm = u.valueL2Norm

Translation preserves the scalar L² norm of a mean-zero H¹ witness.

theorem HCPolySupport.H1MeanZeroFunction.gradientL2Norm_untranslate_eq {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1MeanZeroFunction (translateSet z U)) : (untranslate z u).gradientL2Norm = u.gradientL2Norm

Translation preserves the gradient L² norm of a mean-zero H¹ witness.

noncomputable def HCPolySupport.H1CoerciveEstimate.translate {d : ℕ} {U : Set (Vec d)} (hC : H1CoerciveEstimate U) (z : Vec d) : H1CoerciveEstimate (translateSet z U)

Translate a coercive H¹ estimate from U to U + z without changing its constant.

Equations

• hC.translate z = { constantValue := hC.constantValue, constant_nonneg := ⋯, bound := ⋯ }

@[simp]

theorem HCPolySupport.H1CoerciveEstimate.translate_constant {d : ℕ} {U : Set (Vec d)} (hC : H1CoerciveEstimate U) (z : Vec d) : (hC.translate z).constantValue = hC.constantValue