Coarse-graining support: Support.PDE.HarmonicTranslation

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

Translation of harmonic functions

This file contains the PDE-level translation API for AHarmonicFunction. It is used by both coarse-graining response identities and cube/open-cube transport.

@[simp]

theorem HCPolySupport.translateCoeffField_neg_add_cancel {d : ℕ} (z : Vec d) (a : CoeffField d) : translateCoeffField (-z) (translateCoeffField z a) = a

theorem HCPolySupport.isAHarmonicGradient_translateSet {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (z : Vec d) {f : Vec d → Vec d} (hf : IsAHarmonicGradient (translateCoeffField z a) U f) : IsAHarmonicGradient a (translateSet z U) fun (x : Vec d) => f (x - z)

noncomputable def HCPolySupport.AHarmonicFunction.translate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (z : Vec d) (u : AHarmonicFunction (translateCoeffField z a) U) : AHarmonicFunction a (translateSet z U)

Translate an a(· + z)-harmonic function on U to an a-harmonic function on U + z.

Equations

• HCPolySupport.AHarmonicFunction.translate z u = { toH1 := u.toH1.translate z, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_translate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (z : Vec d) (u : AHarmonicFunction (translateCoeffField z a) U) (x : Vec d) : (translate z u).toH1.grad x = u.toH1.grad (x - z)