Coarse-graining support: Support.Book.Ch04.Theorems.CanonicalSolutions.Definitions

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

Canonical solution-field measurability

This file is the public Ch4 handoff for selected canonical doubled-Mu Hilbert minimizers. The definition below is total: on coefficient fields that lie in some AEE quantitative slice it uses the least slice index, and outside that support it returns 0. Under a RestrictionLawCarrier, the outside branch is null.

noncomputable def HCPolySupport.Book.Ch04.canonicalMuHilbertMinimizerCubeSet {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) : CoeffField d → ↥(HilbertBlockL2 (cubeSet Q))

The canonical totalized selected doubled-Mu Hilbert minimizer on a deterministic cube. On fields that belong to some AEE quantitative slice it uses the least such slice index; outside the AEE slice cover it is 0.

The law-facing theorem RestrictionLawCarrier.aestronglyMeasurable_canonicalMuHilbertMinimizer_cubeSet shows that this totalization is harmless under a RestrictionLawCarrier.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalMuHilbertPotentialCubeSet {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) : CoeffField d → ↥(HilbertVectorL2 (cubeSet Q))

Potential component of the selected doubled-Mu Hilbert minimizer on a deterministic cube.

Equations

• HCPolySupport.Book.Ch04.canonicalMuHilbertPotentialCubeSet Q P0 a = HCPolySupport.hilbertBlockL2PotentialCLM (HCPolySupport.Book.Ch04.canonicalMuHilbertMinimizerCubeSet Q P0 a)

noncomputable def HCPolySupport.Book.Ch04.canonicalMuHilbertFluxCubeSet {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) : CoeffField d → ↥(HilbertVectorL2 (cubeSet Q))

Flux component of the selected doubled-Mu Hilbert minimizer on a deterministic cube.

Equations

• HCPolySupport.Book.Ch04.canonicalMuHilbertFluxCubeSet Q P0 a = HCPolySupport.hilbertBlockL2FluxCLM (HCPolySupport.Book.Ch04.canonicalMuHilbertMinimizerCubeSet Q P0 a)

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialFieldCubeSet {d : ℕ} (Q : TriadicCube d) (p q : Vec d) : CoeffField d → ↥(HilbertVectorL2 (cubeSet Q))

Ch4 selected doubled-Mu potential field with response loading (-p, q).

This object is measurable and useful for the doubled-Mu problem, but it is not, by definition, the raw scalar response-maximizer gradient ∇ v(·, Q, p, q; a). Section 5.3 weak norms should use the scalar-response average and weak-norm observables below, which add the selected doubled-Mu projection to its coefficient-operator image averages.

Equations

• HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialFieldCubeSet Q p q = HCPolySupport.Book.Ch04.canonicalMuHilbertPotentialCubeSet Q (-p, q)

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxFieldCubeSet {d : ℕ} (Q : TriadicCube d) (p q : Vec d) : CoeffField d → ↥(HilbertVectorL2 (cubeSet Q))

Ch4 selected doubled-Mu flux field with response loading (-p, q).

This is the flux projection of the selected doubled-Mu minimizer. It is not, by definition, the raw scalar response flux a ∇ v(·, Q, p, q; a).

Equations

• HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxFieldCubeSet Q p q = HCPolySupport.Book.Ch04.canonicalMuHilbertFluxCubeSet Q (-p, q)

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialFieldAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

The selected doubled-Mu potential field averaged over R, viewed as a continuous postcomposition of the parent-cube Hilbert L² field on Q.

The intended use is R ∈ descendantsAtDepth Q j, but the definition is total.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxFieldAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

The selected doubled-Mu flux field averaged over R, viewed as a continuous postcomposition of the parent-cube Hilbert L² field on Q.

The intended use is R ∈ descendantsAtDepth Q j, but the definition is total.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.descendantsAverageCanonicalDoubledMuResponsePotentialFieldAverageCubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : CoeffField d → Vec d

Finite descendant average of the selected doubled-Mu potential averages.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.descendantsAverageCanonicalDoubledMuResponseFluxFieldAverageCubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : CoeffField d → Vec d

Finite descendant average of the selected doubled-Mu flux averages.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialWeakNormPartialCubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (p q p0 : Vec d) : CoeffField d → ℝ

Finite-depth selected doubled-Mu potential weak norm, expressed only through descendant averages of the selected doubled-Mu Hilbert field.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxWeakNormPartialCubeSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) (N : ℕ) (p q q0 : Vec d) : CoeffField d → ℝ

Finite-depth selected doubled-Mu flux weak norm, expressed only through descendant averages of the selected doubled-Mu Hilbert field.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialWeakNormCubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) : CoeffField d → ℝ

Full selected doubled-Mu potential weak norm, as the countable supremum of the finite-depth norms.

Equations

• HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialWeakNormCubeSet Q s p q p0 a = ⨆ (N : ℕ), HCPolySupport.Book.Ch04.canonicalDoubledMuResponsePotentialWeakNormPartialCubeSet Q s N p q p0 a

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxWeakNormCubeSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) (p q q0 : Vec d) : CoeffField d → ℝ

Full selected doubled-Mu flux weak norm, as the countable supremum of the finite-depth norms.

Equations

• HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxWeakNormCubeSet Q t p q q0 a = ⨆ (N : ℕ), HCPolySupport.Book.Ch04.canonicalDoubledMuResponseFluxWeakNormPartialCubeSet Q t N p q q0 a

noncomputable def HCPolySupport.Book.Ch04.canonicalMuHilbertEnergyBilinFixedCubeSet {d : ℕ} (Q : TriadicCube d) (P0 : BlockVec d) (Y : BlockState d) (hY : MemBlockL2 (cubeSet Q) Y.eval) : CoeffField d → ℝ

Totalized fixed-test Hilbert energy pairing against the selected canonical doubled-Mu minimizer. On the AEE elliptic support it uses the least quantitative slice; outside that support it is set to 0.

This is an internal Ch4 scalar-response source: fixed indicator tests recover averages of the coefficient-operator image of the selected minimizer.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalUpperImageIndicatorTestStateCubeSet {d : ℕ} (R : TriadicCube d) (i : Fin d) : BlockState d

A block test state with the cube indicator times the ith basis vector in its potential component and zero flux.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalLowerImageIndicatorTestStateCubeSet {d : ℕ} (R : TriadicCube d) (i : Fin d) : BlockState d

A block test state with the cube indicator times the ith basis vector in its flux component and zero potential.

Equations

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

theorem HCPolySupport.Book.Ch04.canonicalUpperImageIndicatorTestStateCubeSet_memBlockL2 {d : ℕ} (Q R : TriadicCube d) (i : Fin d) : MemBlockL2 (cubeSet Q) (canonicalUpperImageIndicatorTestStateCubeSet R i).eval

theorem HCPolySupport.Book.Ch04.canonicalLowerImageIndicatorTestStateCubeSet_memBlockL2 {d : ℕ} (Q R : TriadicCube d) (i : Fin d) : MemBlockL2 (cubeSet Q) (canonicalLowerImageIndicatorTestStateCubeSet R i).eval

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseUpperImageAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

Average over R of the upper component of the coefficient-operator image of the selected doubled-Mu minimizer on Q.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalDoubledMuResponseLowerImageAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

Average over R of the lower component of the coefficient-operator image of the selected doubled-Mu minimizer on Q.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseGradientAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

Ch4 measurable representative of the raw scalar response-maximizer gradient average over a descendant cube R.

Mathematically this is avg_R grad v(·, Q, p, q; a): it is extracted from the selected doubled-Mu minimizer by adding its potential projection and the lower coefficient-operator image.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseFluxAverageCubeSet {d : ℕ} (Q R : TriadicCube d) (p q : Vec d) : CoeffField d → Vec d

Ch4 measurable representative of the raw scalar response-maximizer flux average over a descendant cube R.

Mathematically this is avg_R a grad v(·, Q, p, q; a): it is extracted from the selected doubled-Mu minimizer by adding its flux projection and the upper coefficient-operator image.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseGradientWeakNormPartialCubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (p q p0 : Vec d) : CoeffField d → ℝ

Finite-depth weak norm of the raw scalar response-maximizer gradient defect grad v_m - p0.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseFluxWeakNormPartialCubeSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) (N : ℕ) (p q q0 : Vec d) : CoeffField d → ℝ

Finite-depth weak norm of the raw scalar response-maximizer flux defect a grad v_m - q0.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseGradientWeakNormCubeSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) : CoeffField d → ℝ

Full weak norm of the raw scalar response-maximizer gradient defect.

Equations

• HCPolySupport.Book.Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a = ⨆ (N : ℕ), HCPolySupport.Book.Ch04.canonicalScalarResponseGradientWeakNormPartialCubeSet Q s N p q p0 a

noncomputable def HCPolySupport.Book.Ch04.canonicalScalarResponseFluxWeakNormCubeSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) (p q q0 : Vec d) : CoeffField d → ℝ

Full weak norm of the raw scalar response-maximizer flux defect.

Equations

• HCPolySupport.Book.Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a = ⨆ (N : ℕ), HCPolySupport.Book.Ch04.canonicalScalarResponseFluxWeakNormPartialCubeSet Q t N p q q0 a

theorem HCPolySupport.Book.Ch04.exists_isBlockMuAdmissible_cube_and_hilbert_eq_canonicalAEEMuHilbertMinimizer {d : ℕ} [NeZero d] (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P0 : BlockVec d) (aQ : Ch02.CoeffOn (Ch02.cubeDomain Q)) (haQ : aQ.toCoeffField = ↑a) {X : Ch02.DoubledField d} (hX : Ch02.IsDoubledMuMinimizer (Ch02.cubeDomain Q) aQ P0 X) : ∃ (hAdm : IsBlockMuAdmissible (cubeSet Q) P0 { potential := X.potential, flux := X.flux }), toHilbertBlockL2OfBlockField ⋯ = (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.minimizerMap P0

A pointwise Ch2 doubled-Mu minimizer on the open cube represents the canonical Ch4 Hilbert minimizer selected on the corresponding half-open cube.

This is the bridge from the pointwise variational theorem used by Ch2 extraction to the measurable Hilbert minimizer used by Ch4.