Coarse-graining support: Support.PDE.Harmonic

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

def HCPolySupport.IsAHarmonicGradient {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (f : Vec d → Vec d) : Prop

An H¹ potential gradient whose coefficient flux pairs to zero with every H¹₀(U) gradient.

Equations

• HCPolySupport.IsAHarmonicGradient a U f = (HCPolySupport.IsPotentialOn U f ∧ HCPolySupport.IsSolenoidalOn U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a x) (f x))

theorem HCPolySupport.IsAHarmonicGradient.of_ae_eq_coeff {d : ℕ} {a b : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (h : a =ᵐ[volumeMeasureOn U] b) (hf : IsAHarmonicGradient a U f) : IsAHarmonicGradient b U f

def HCPolySupport.IsAHarmonicPair {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (f g : Vec d → Vec d) : Prop

A potential field and solenoidal flux on U, with g = a f pointwise everywhere.

Equations

• HCPolySupport.IsAHarmonicPair a U f g = (HCPolySupport.IsPotentialOn U f ∧ HCPolySupport.IsSolenoidalOn U g ∧ ∀ (x : HCPolySupport.Vec d), g x = HCPolySupport.matVecMul (a x) (f x))

def HCPolySupport.IsAdjointHarmonicPair {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (f g : Vec d → Vec d) : Prop

A potential field and solenoidal flux on U, with g = aᵀ f pointwise everywhere.

Equations

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

structure HCPolySupport.AHarmonicPair {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) : Type

A pair of potential and flux fields satisfying the a-harmonic relation on U.

• grad : Vec d → Vec d

  The potential field of the harmonic pair.

• flux : Vec d → Vec d

  The solenoidal flux, pointwise equal to the coefficient applied to the potential field.

• isHarmonicPair : IsAHarmonicPair a U self.grad self.flux

structure HCPolySupport.AHarmonicFunction {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) : Type

An H¹(U) function whose coefficient-weighted weak gradient is solenoidal on U.

• toH1 : H1Function U

  The underlying H¹ function and its weak gradient.

• isHarmonic : IsAHarmonicGradient a U self.toH1.grad

@[reducible, inline]

abbrev HCPolySupport.h10FluxIntegrable {d : ℕ} (U : Set (Vec d)) (F : Vec d → Vec d) : Prop

Integrability of a vector flux paired with every H10Function test gradient. This abbreviation keeps harmonic-combination headers small.

Equations

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

@[reducible, inline]

abbrev HCPolySupport.weakFluxIntegrable {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (u : AHarmonicFunction a U) : Prop

Integrability of the weak flux pairing attached to an AHarmonicFunction.

Equations

• HCPolySupport.weakFluxIntegrable U a u = HCPolySupport.h10FluxIntegrable U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a x) (u.toH1.grad x)

@[reducible, inline]

abbrev HCPolySupport.AStarHarmonicFunction {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

Surface notation for adjoint-harmonic functions. This matches the Chapter-2 notation 𝒜*(U; a) while reusing the existing AHarmonicFunction structure.

Equations

• HCPolySupport.AStarHarmonicFunction U a = HCPolySupport.AHarmonicFunction (fun (x : HCPolySupport.Vec d) => HCPolySupport.matTranspose (a x)) U

structure HCPolySupport.AHarmonicFunctionMeanZero {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) : Type

An a-harmonic H¹ function with zero integral over U.

• toAHarmonicFunction : AHarmonicFunction a U

  The underlying harmonic function with zero integral.

• meanZero : MeanZeroOn U self.toAHarmonicFunction.toH1.toFun

@[instance_reducible]

instance HCPolySupport.AHarmonicFunctionMeanZero.instCoeAHarmonicFunction {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : Coe (AHarmonicFunctionMeanZero a U) (AHarmonicFunction a U)

Equations

• HCPolySupport.AHarmonicFunctionMeanZero.instCoeAHarmonicFunction = { coe := fun (u : HCPolySupport.AHarmonicFunctionMeanZero a U) => u.toAHarmonicFunction }

@[simp]

theorem HCPolySupport.AHarmonicFunctionMeanZero.coe_mk {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) (hmean : MeanZeroOn U u.toH1.toFun) : { toAHarmonicFunction := u, meanZero := hmean }.toAHarmonicFunction = u

theorem HCPolySupport.AHarmonicFunctionMeanZero.meanZero_coe {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunctionMeanZero a U) : MeanZeroOn U u.toAHarmonicFunction.toH1.toFun

theorem HCPolySupport.isAHarmonicGradient_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : IsAHarmonicGradient a U 0

theorem HCPolySupport.isAHarmonicGradient_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) (c : ℝ) : IsAHarmonicGradient a U (c • f)

theorem HCPolySupport.isAHarmonicGradient_add_of_integrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) (hg : IsAHarmonicGradient a U g) (hf_int : h10FluxIntegrable U fun (x : Vec d) => matVecMul (a x) (f x)) (hg_int : h10FluxIntegrable U fun (x : Vec d) => matVecMul (a x) (g x)) : IsAHarmonicGradient a U (f + g)

theorem HCPolySupport.isAHarmonicPair_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : IsAHarmonicPair a U 0 0

theorem HCPolySupport.isAHarmonicPair_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : IsAHarmonicPair a U f g) (c : ℝ) : IsAHarmonicPair a U (c • f) (c • g)

theorem HCPolySupport.isAHarmonicPair_add_of_integrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f1 g1 f2 g2 : Vec d → Vec d} (h1 : IsAHarmonicPair a U f1 g1) (h2 : IsAHarmonicPair a U f2 g2) (hg1_int : h10FluxIntegrable U g1) (hg2_int : h10FluxIntegrable U g2) : IsAHarmonicPair a U (f1 + f2) (g1 + g2)

theorem HCPolySupport.isAHarmonicPair_of_isAHarmonicGradient {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) : IsAHarmonicPair a U f fun (x : Vec d) => matVecMul (a x) (f x)

theorem HCPolySupport.isAHarmonicGradient_of_isAHarmonicPair {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : IsAHarmonicPair a U f g) : IsAHarmonicGradient a U f

theorem HCPolySupport.IsAHarmonicGradient.restrict_of_isOpen_of_memVectorL2 {d : ℕ} {a : CoeffField d} {U V : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hfluxV : MemVectorL2 V fun (x : Vec d) => matVecMul (a x) (f x)) : IsAHarmonicGradient a V f

theorem HCPolySupport.IsAHarmonicGradient.restrict_of_isOpen_of_isEllipticFieldOn {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {U V : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hEllV : IsEllipticFieldOn lam Lam V a) : IsAHarmonicGradient a V f

theorem HCPolySupport.isAdjointHarmonicPair_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : IsAdjointHarmonicPair a U 0 0

theorem HCPolySupport.isAdjointHarmonicPair_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : IsAdjointHarmonicPair a U f g) (c : ℝ) : IsAdjointHarmonicPair a U (c • f) (c • g)

theorem HCPolySupport.isAdjointHarmonicPair_add_of_integrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f1 g1 f2 g2 : Vec d → Vec d} (h1 : IsAdjointHarmonicPair a U f1 g1) (h2 : IsAdjointHarmonicPair a U f2 g2) (hg1_int : h10FluxIntegrable U g1) (hg2_int : h10FluxIntegrable U g2) : IsAdjointHarmonicPair a U (f1 + f2) (g1 + g2)

theorem HCPolySupport.AHarmonicPair.ext {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X Y : AHarmonicPair a U} (hgrad : X.grad = Y.grad) (hflux : X.flux = Y.flux) : X = Y

theorem HCPolySupport.AHarmonicPair.ext_iff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X Y : AHarmonicPair a U} : X = Y ↔ X.grad = Y.grad ∧ X.flux = Y.flux

@[instance_reducible]

instance HCPolySupport.AHarmonicPair.instZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : Zero (AHarmonicPair a U)

Equations

• HCPolySupport.AHarmonicPair.instZero = { zero := { grad := 0, flux := 0, isHarmonicPair := ⋯ } }

@[instance_reducible]

instance HCPolySupport.AHarmonicPair.instSMulReal {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : SMul ℝ (AHarmonicPair a U)

Equations

• HCPolySupport.AHarmonicPair.instSMulReal = { smul := fun (c : ℝ) (X : HCPolySupport.AHarmonicPair a U) => { grad := c • X.grad, flux := c • X.flux, isHarmonicPair := ⋯ } }

@[simp]

theorem HCPolySupport.AHarmonicPair.grad_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : grad 0 = 0

@[simp]

theorem HCPolySupport.AHarmonicPair.flux_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} : flux 0 = 0

@[simp]

theorem HCPolySupport.AHarmonicPair.grad_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (X : AHarmonicPair a U) : (c • X).grad = c • X.grad

@[simp]

theorem HCPolySupport.AHarmonicPair.flux_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (c : ℝ) (X : AHarmonicPair a U) : (c • X).flux = c • X.flux

def HCPolySupport.AHarmonicPair.ofGradient {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) : AHarmonicPair a U

Pair a harmonic gradient with its coefficient flux.

Equations

• HCPolySupport.AHarmonicPair.ofGradient hf = { grad := f, flux := fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a x) (f x), isHarmonicPair := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicPair.grad_ofGradient {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) : (ofGradient hf).grad = f

@[simp]

theorem HCPolySupport.AHarmonicPair.flux_ofGradient {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsAHarmonicGradient a U f) : (ofGradient hf).flux = fun (x : Vec d) => matVecMul (a x) (f x)

def HCPolySupport.AHarmonicPair.addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (X Y : AHarmonicPair a U) (hX_int : h10FluxIntegrable U X.flux) (hY_int : h10FluxIntegrable U Y.flux) : AHarmonicPair a U

Add harmonic pairs componentwise when their flux pairings with zero-trace tests are integrable.

Equations

• X.addOfIntegrable Y hX_int hY_int = { grad := X.grad + Y.grad, flux := X.flux + Y.flux, isHarmonicPair := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicPair.grad_addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (X Y : AHarmonicPair a U) (hX_int : h10FluxIntegrable U X.flux) (hY_int : h10FluxIntegrable U Y.flux) : (X.addOfIntegrable Y hX_int hY_int).grad = X.grad + Y.grad

@[simp]

theorem HCPolySupport.AHarmonicPair.flux_addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (X Y : AHarmonicPair a U) (hX_int : h10FluxIntegrable U X.flux) (hY_int : h10FluxIntegrable U Y.flux) : (X.addOfIntegrable Y hX_int hY_int).flux = X.flux + Y.flux

def HCPolySupport.AHarmonicFunction.toPair {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) : AHarmonicPair a U

The harmonic pair consisting of the function's weak gradient and coefficient flux.

Equations

• u.toPair = HCPolySupport.AHarmonicPair.ofGradient ⋯

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

Add a scalar constant to a harmonic function on a finite-measure domain.

Equations

• u.addConst c = { toH1 := u.toH1.addConst c, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_addConst {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) (c : ℝ) : (u.addConst c).toH1 = u.toH1.addConst c

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

@[simp]

theorem HCPolySupport.AHarmonicFunction.toPair_addConst {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) (c : ℝ) : (u.addConst c).toPair = u.toPair

noncomputable def HCPolySupport.AHarmonicFunction.normalizeMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : AHarmonicFunction a U

Subtract the volume average from a harmonic function.

Equations

• u.normalizeMeanZero = { toH1 := u.toH1.subAverage, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_normalizeMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : u.normalizeMeanZero.toH1 = u.toH1.subAverage

theorem HCPolySupport.AHarmonicFunction.meanZeroOn_normalizeMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : MeanZeroOn U u.normalizeMeanZero.toH1.toFun

theorem HCPolySupport.AHarmonicFunction.grad_normalizeMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) (x : Vec d) : u.normalizeMeanZero.toH1.grad x = u.toH1.grad x

noncomputable def HCPolySupport.AHarmonicFunction.toMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : AHarmonicFunctionMeanZero a U

Package a harmonic function after subtracting its volume average as a mean-zero harmonic function.

Equations

• u.toMeanZero = { toAHarmonicFunction := u.normalizeMeanZero, meanZero := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.coe_toMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : u.toMeanZero.toAHarmonicFunction = u.normalizeMeanZero

theorem HCPolySupport.AHarmonicFunction.meanZero_toMeanZero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : AHarmonicFunction a U) : MeanZeroOn U u.toMeanZero.toAHarmonicFunction.toH1.toFun

theorem HCPolySupport.AHarmonicFunction.integrableOn_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (c : ℝ) : h10FluxIntegrable U fun (x : Vec d) => matVecMul (a x) ((c • u.toH1).grad x)

noncomputable def HCPolySupport.AHarmonicFunction.restrictOfMemVectorL2 {d : ℕ} {a : CoeffField d} {U V : Set (Vec d)} (u : AHarmonicFunction a U) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hfluxV : MemVectorL2 V fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) : AHarmonicFunction a V

Restrict a harmonic function to an open subset with square-integrable coefficient flux.

Equations

• u.restrictOfMemVectorL2 hU hV hVU hfluxV = { toH1 := u.toH1.restrict hV hVU, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_restrictOfMemVectorL2 {d : ℕ} {a : CoeffField d} {U V : Set (Vec d)} (u : AHarmonicFunction a U) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hfluxV : MemVectorL2 V fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) : (u.restrictOfMemVectorL2 hU hV hVU hfluxV).toH1 = u.toH1.restrict hV hVU

noncomputable def HCPolySupport.AHarmonicFunction.restrictOfIsEllipticFieldOn {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {U V : Set (Vec d)} (u : AHarmonicFunction a U) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hEllV : IsEllipticFieldOn lam Lam V a) : AHarmonicFunction a V

Restrict a harmonic function to an open subset where the coefficient field is elliptic.

Equations

• u.restrictOfIsEllipticFieldOn hU hV hVU hEllV = u.restrictOfMemVectorL2 hU hV hVU ⋯

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_restrictOfIsEllipticFieldOn {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {U V : Set (Vec d)} (u : AHarmonicFunction a U) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hEllV : IsEllipticFieldOn lam Lam V a) : (u.restrictOfIsEllipticFieldOn hU hV hVU hEllV).toH1 = u.toH1.restrict hV hVU

def HCPolySupport.AHarmonicFunction.addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : AHarmonicFunction a U

Add harmonic functions whose weak flux pairings are integrable.

Equations

• u.addOfIntegrable v hu_int hv_int = { toH1 := u.toH1 + v.toH1, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : (u.addOfIntegrable v hu_int hv_int).toH1 = u.toH1 + v.toH1

theorem HCPolySupport.AHarmonicFunction.grad_addOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u v : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hv_int : weakFluxIntegrable U a v) : (u.addOfIntegrable v hu_int hv_int).toH1.grad = u.toH1.grad + v.toH1.grad

def HCPolySupport.AHarmonicFunction.addSMulOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) (c : ℝ) : AHarmonicFunction a U

Form the harmonic function u + c • w using integrable weak flux pairings.

Equations

• u.addSMulOfIntegrable w hu_int hw_int c = u.addOfIntegrable { toH1 := c • w.toH1, isHarmonic := ⋯ } hu_int ⋯

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_addSMulOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) (c : ℝ) : (u.addSMulOfIntegrable w hu_int hw_int c).toH1 = u.toH1 + c • w.toH1

theorem HCPolySupport.AHarmonicFunction.grad_addSMulOfIntegrable {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u w : AHarmonicFunction a U) (hu_int : weakFluxIntegrable U a u) (hw_int : weakFluxIntegrable U a w) (c : ℝ) : (u.addSMulOfIntegrable w hu_int hw_int c).toH1.grad = u.toH1.grad + c • w.toH1.grad