Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.CanonicalFields #

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

CanonicalFields #

Canonical scalar maximizer fields and Ch4 extraction identities.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.ch02_coeffOn_isAEEllipticFieldOn {d : ℕ} {U : Ch02.Domain d} (a : Ch02.CoeffOn U) :

IsAEEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField

A Chapter 2 coefficient object is a spatially a.e. elliptic field on its public domain.

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerSolutionOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) :

Ch02.Solution (Ch02.cubeDomain Q) a

Private raw Chapter 2 canonical maximizer on a cube. This is a local Section 5.3 adapter for deterministic estimates; the measurable selected observables remain the Ch4 Hilbert-field definitions.

Equations

HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerSolutionOnCube Q a p q = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p q).toSolution

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotential {d : ℕ} (p0 : Vec d) :

Vec d → ℝ

The affine comparison function ell_p0(x) = p0 dot x, used only inside the private product-term reduction.

Equations

HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotential p0 x = HCPolySupport.vecDot p0 x

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialCLM {d : ℕ} (p0 : Vec d) :

Vec d →L[ℝ ] ℝ

Continuous-linear version of linearPotential, used to compute its Fréchet derivative without exposing another public definition.

Equations

HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialCLM p0 = ∑ i : Fin d, p0 i • ContinuousLinearMap.proj i

Instances For

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotential_eq_linearPotentialCLM {d : ℕ} (p0 : Vec d) :

linearPotential p0 = fun (x : Vec d) => (linearPotentialCLM p0) x

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialCLM_apply_basisVec {d : ℕ} (p0 : Vec d) (i : Fin d) :

(linearPotentialCLM p0) (basisVec i) = p0 i

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.fderiv_linearPotential_apply_basisVec {d : ℕ} (p0 x : Vec d) (i : Fin d) :

(fderiv ℝ (linearPotential p0) x) (basisVec i) = p0 i

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialH1OnCube {d : ℕ} (Q : TriadicCube d) (p0 : Vec d) :

H1Function (Ch02.cubeDomain Q).carrier

ell_p0 as an H¹ function on the parent open cube.

Equations

HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialH1OnCube Q p0 = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯

Instances For

source

@[simp]

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialH1OnCube_toFun {d : ℕ} (Q : TriadicCube d) (p0 : Vec d) :

(linearPotentialH1OnCube Q p0).toFun = linearPotential p0

source

@[simp]

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.linearPotentialH1OnCube_grad {d : ℕ} (Q : TriadicCube d) (p0 : Vec d) :

(linearPotentialH1OnCube Q p0).grad = fun (x : Vec d) => p0

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerPotentialDefectOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

Vec d → ℝ

Private potential defect v_m - ell_p0 for the raw canonical maximizer.

Equations

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

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) :

Vec d → Vec d

Raw gradient field of the canonical maximizer on a cube.

Equations

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

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

Vec d → Vec d

Private gradient defect grad v_m - p0 for the raw canonical maximizer.

Equations

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

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) :

Vec d → Vec d

Raw flux field of the canonical maximizer on a cube.

Equations

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

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q q0 : Vec d) :

Vec d → Vec d

Private flux defect a grad v_m - q0 for the raw canonical maximizer.

Equations

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

Instances For

source

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerPotentialDefectH1OnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

H1Function (Ch02.cubeDomain Q).carrier

v_m - ell_p0 as an H¹ function on the parent open cube.

Equations

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

Instances For

source

@[simp]

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerPotentialDefectH1OnCube_toFun {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

(canonicalMaximizerPotentialDefectH1OnCube Q a p q p0).toFun = canonicalMaximizerPotentialDefectOnCube Q a p q p0

source

@[simp]

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerPotentialDefectH1OnCube_grad {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

(canonicalMaximizerPotentialDefectH1OnCube Q a p q p0).grad = fun (x : Vec d) => canonicalMaximizerGradientOnCube Q a p q x - p0

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerPotentialDefectOnCube_memLp {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

MeasureTheory.MemLp (canonicalMaximizerPotentialDefectOnCube Q a p q p0) 2 (normalizedCubeMeasure Q)

The raw canonical maximizer potential defect is L² on the normalized cube. This is deterministic H¹ membership plus the smooth affine comparison, not a law/measurability fact.

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube_memLp {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) :

MeasureTheory.MemLp (canonicalMaximizerGradientDefectOnCube Q a p q p0) 2 (normalizedCubeMeasure Q)

The raw canonical maximizer gradient defect is L² on the normalized cube.

source

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube_memLp {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q q0 : Vec d) :

MeasureTheory.MemLp (canonicalMaximizerFluxDefectOnCube Q a p q q0) 2 (normalizedCubeMeasure Q)

The raw canonical maximizer flux defect is L² on the normalized cube.

The coefficient object is only a.e.-elliptic, so the flux bound is delegated to the public Ch2 source theorem Solution.flux_memVectorL2, which hides the pointwise-good representative used in its proof.

source