Coarse-graining support: Support.Book.Ch02.Setup

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

structure HCPolySupport.Book.Ch02.Domain (d : ℕ) : Type

Public Chapter 2 domains: nonempty bounded open convex subsets of R^d.

• carrier : Set (Vec d)

  The nonempty bounded open convex set underlying the domain.

• isDomain : IsOpenBoundedConvexDomain self.carrier
• nonempty : self.carrier.Nonempty

@[instance_reducible]

instance HCPolySupport.Book.Ch02.Domain.instCoeSetVec {d : ℕ} : Coe (Domain d) (Set (Vec d))

Equations

• HCPolySupport.Book.Ch02.Domain.instCoeSetVec = { coe := fun (U : HCPolySupport.Book.Ch02.Domain d) => U.carrier }

@[simp]

theorem HCPolySupport.Book.Ch02.Domain.coe_mk {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : { carrier := U, isDomain := hU, nonempty := hne }.carrier = U

theorem HCPolySupport.Book.Ch02.Domain.isOpen {d : ℕ} (U : Domain d) : IsOpen U.carrier

theorem HCPolySupport.Book.Ch02.Domain.isBoundedDomain {d : ℕ} (U : Domain d) : IsBoundedDomain U.carrier

theorem HCPolySupport.Book.Ch02.Domain.convex {d : ℕ} (U : Domain d) : Convex ℝ U.carrier

theorem HCPolySupport.Book.Ch02.Domain.measurableSet {d : ℕ} (U : Domain d) : MeasurableSet U.carrier

instance HCPolySupport.Book.Ch02.Domain.instIsFiniteMeasureVolumeMeasureOn {d : ℕ} (U : Domain d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)

structure HCPolySupport.Book.Ch02.CoeffOn {d : ℕ} (U : Domain d) : Type

Public version of a in Omega(U).

This is deliberately an almost-everywhere object: the coefficient field is a representative, and all public regularity/ellipticity data is stated with respect to volumeMeasureOn U.

• toCoeffField : CoeffField d

  The representative matrix-valued coefficient field on the domain.

• lam : ℝ

  The positive lower ellipticity parameter of the coefficient field on the domain.

• Lam : ℝ

  The upper ellipticity parameter of the coefficient field on the domain.

• lam_pos : 0 < self.lam
• lam_le_Lam : self.lam ≤ self.Lam
• aeStronglyMeasurable (i j : Fin d) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => restrictCoeffField U.carrier self.toCoeffField x i j) (volumeMeasureOn U.carrier)
• aeElliptic : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, IsEllipticMatrix self.lam self.Lam (self.toCoeffField x)

@[instance_reducible]

instance HCPolySupport.Book.Ch02.CoeffOn.instCoeFunCoeffField {d : ℕ} {U : Domain d} : CoeFun (CoeffOn U) fun (x : CoeffOn U) => CoeffField d

Equations

• HCPolySupport.Book.Ch02.CoeffOn.instCoeFunCoeffField = { coe := fun (a : HCPolySupport.Book.Ch02.CoeffOn U) => a.toCoeffField }

theorem HCPolySupport.Book.Ch02.CoeffOn.measurableSet {d : ℕ} {U : Domain d} (_a : CoeffOn U) : MeasurableSet U.carrier

noncomputable def HCPolySupport.Book.Ch02.CoeffOn.transpose {d : ℕ} {U : Domain d} (a : CoeffOn U) : CoeffOn U

Public adjoint coefficient field a^t, still as an a.e. coefficient object on the same Chapter 2 domain.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch02.CoeffOn.transpose_apply {d : ℕ} {U : Domain d} (a : CoeffOn U) (x : Vec d) : a.transpose.toCoeffField x = matTranspose (a.toCoeffField x)

def HCPolySupport.Book.Ch02.CoeffOn.AEEq {d : ℕ} {U : Domain d} (a b : CoeffOn U) : Prop

Equality of public coefficient fields is equality of representatives almost everywhere on the public domain.

Equations

• a.AEEq b = (a.toCoeffField =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] b.toCoeffField)

def HCPolySupport.Book.Ch02.CoeffOn.IsSymmetric {d : ℕ} {U : Domain d} (a : CoeffOn U) : Prop

Public a.e. symmetry predicate for coefficient representatives.

The Chapter 2 public layer deliberately does not use pointwise symmetry as a theorem hypothesis.

Equations

• a.IsSymmetric = ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U.carrier, Matrix.IsSymm (a.toCoeffField x)

def HCPolySupport.Book.Ch02.CoeffOn.AEScaled {d : ℕ} {U : Domain d} (c : ℝ) (a b : CoeffOn U) : Prop

b is the a.e. scalar rescaling c a on the public domain.

Equations

• HCPolySupport.Book.Ch02.CoeffOn.AEScaled c a b = (b.toCoeffField =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => c • a.toCoeffField x)

def HCPolySupport.Book.Ch02.CoeffOn.RestrictsTo {d : ℕ} {U V : Domain d} (a : CoeffOn U) (b : CoeffOn V) : Prop

b is the restriction of a to a smaller public domain, modulo null sets.

This is deliberately an a.e. relation between coefficient representatives, rather than a pointwise restriction definition.

Equations

• a.RestrictsTo b = (b.toCoeffField =ᵐ[HCPolySupport.volumeMeasureOn V.carrier] a.toCoeffField)

theorem HCPolySupport.Book.Ch02.CoeffOn.AEEq.refl {d : ℕ} {U : Domain d} (a : CoeffOn U) : a.AEEq a

theorem HCPolySupport.Book.Ch02.CoeffOn.AEEq.symm {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : b.AEEq a

theorem HCPolySupport.Book.Ch02.CoeffOn.AEEq.trans {d : ℕ} {U : Domain d} {a b c : CoeffOn U} (hab : a.AEEq b) (hbc : b.AEEq c) : a.AEEq c

theorem HCPolySupport.Book.Ch02.CoeffOn.AEEq.transpose {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : a.transpose.AEEq b.transpose

theorem HCPolySupport.Book.Ch02.CoeffOn.transpose_transpose_aeeq {d : ℕ} {U : Domain d} (a : CoeffOn U) : a.transpose.transpose.AEEq a

@[reducible, inline]

abbrev HCPolySupport.Book.Ch02.Solution {d : ℕ} (U : Domain d) (a : CoeffOn U) : Type

Public Chapter 2 notation for A(U; a).

Equations

• HCPolySupport.Book.Ch02.Solution U a = HCPolySupport.AHarmonicFunction a.toCoeffField U.carrier

def HCPolySupport.Book.Ch02.Solution.SameGradientAE {d : ℕ} {U : Domain d} {a : CoeffOn U} (u v : Solution U a) : Prop

Two public solutions have the same gradient on U, modulo null sets.

Equations

• u.SameGradientAE v = (u.toH1.grad =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] v.toH1.grad)

theorem HCPolySupport.Book.Ch02.Solution.SameGradientAE.refl {d : ℕ} {U : Domain d} {a : CoeffOn U} (u : Solution U a) : u.SameGradientAE u

theorem HCPolySupport.Book.Ch02.Solution.SameGradientAE.symm {d : ℕ} {U : Domain d} {a : CoeffOn U} {u v : Solution U a} (h : u.SameGradientAE v) : v.SameGradientAE u

theorem HCPolySupport.Book.Ch02.Solution.SameGradientAE.trans {d : ℕ} {U : Domain d} {a : CoeffOn U} {u v w : Solution U a} (huv : u.SameGradientAE v) (hvw : v.SameGradientAE w) : u.SameGradientAE w

def HCPolySupport.Book.Ch02.Solution.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (u : Solution U a) : Solution U b

Transport a solution across a change of coefficient representative on a null set.

Equations

• HCPolySupport.Book.Ch02.Solution.ofAEEq h u = { toH1 := u.toH1, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch02.Solution.toH1_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (u : Solution U a) : (ofAEEq h u).toH1 = u.toH1

@[simp]

theorem HCPolySupport.Book.Ch02.Solution.ofAEEq_refl {d : ℕ} {U : Domain d} {a : CoeffOn U} (u : Solution U a) : ofAEEq ⋯ u = u

theorem HCPolySupport.Book.Ch02.Solution.sameGradientAE_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {u v : Solution U a} (huv : u.SameGradientAE v) : (ofAEEq h u).SameGradientAE (ofAEEq h v)

@[reducible, inline]

abbrev HCPolySupport.Book.Ch02.AdjointSolution {d : ℕ} (U : Domain d) (a : CoeffOn U) : Type

Public Chapter 2 notation for the adjoint solution space A*(U; a).

Equations

• HCPolySupport.Book.Ch02.AdjointSolution U a = HCPolySupport.AStarHarmonicFunction U.carrier a.toCoeffField

def HCPolySupport.Book.Ch02.zeroSolution {d : ℕ} (U : Domain d) (a : CoeffOn U) : Solution U a

The zero solution, used to show that the response supremum is over a nonempty set.

Equations

• HCPolySupport.Book.Ch02.zeroSolution U a = { toH1 := 0, isHarmonic := ⋯ }