Coarse-graining support: Support.CoarseGraining.MuOperator.AEEOperator.CanonicalCubeSet

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

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.toAEEMuOperatorSystemData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : PotentialSolenoidalL2Data U) (coeffOperatorData : AEEMuCoeffOperatorData U a) : AEEMuOperatorSystemData U a

Build the AEE doubled operator system from a packaged correction space and a.e.-representative coefficient-operator data.

Equations

• M.toAEEMuOperatorSystemData coeffOperatorData = { correctionSpace := M.toMuCorrectionSpaceData, coeffOperatorData := coeffOperatorData }

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.toAEEMuOperatorSystemDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : PotentialSolenoidalL2Data U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : AEEMuOperatorSystemData U a

Build the AEE doubled operator system from the old pointwise elliptic constructor. This is a compatibility bridge; the genuinely new Phase 3 constructor will start from spatial-a.e. ellipticity instead.

Equations

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

@[simp]

theorem HCPolySupport.PotentialSolenoidalL2Data.correctionSpace_toAEEMuOperatorSystemData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : PotentialSolenoidalL2Data U) (coeffOperatorData : AEEMuCoeffOperatorData U a) : (M.toAEEMuOperatorSystemData coeffOperatorData).correctionSpace = M.toMuCorrectionSpaceData

@[instance 900]

instance HCPolySupport.instIsFiniteMeasureVolumeMeasureOnCubeSetAEEOperator {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))

Half-open triadic cubes carry finite restricted volume measure.

theorem HCPolySupport.volume_cubeSet_toReal_pos {d : ℕ} (Q : TriadicCube d) : 0 < (MeasureTheory.volume (cubeSet Q)).toReal

Half-open triadic cubes have positive volume in toReal form.

noncomputable def HCPolySupport.canonicalAEEPotentialSolenoidalL2Data {d : ℕ} (Q : TriadicCube d) : PotentialSolenoidalL2Data (cubeSet Q)

Canonical potential/solenoidal L² data used by the AEE cube-set operator system.

Equations

• HCPolySupport.canonicalAEEPotentialSolenoidalL2Data Q = HCPolySupport.PotentialSolenoidalL2Data.ofSubmoduleClosures (HCPolySupport.cubeSet Q)

noncomputable def HCPolySupport.canonicalAEEMuCorrectionSpaceData {d : ℕ} (Q : TriadicCube d) : MuCorrectionSpaceData (cubeSet Q)

Canonical Hilbert correction space for the AEE doubled \mu problem on a half-open triadic cube.

Equations

• HCPolySupport.canonicalAEEMuCorrectionSpaceData Q = (HCPolySupport.canonicalAEEPotentialSolenoidalL2Data Q).toMuCorrectionSpaceData

instance HCPolySupport.canonicalAEEMuCorrectionSpaceData_separable {d : ℕ} (Q : TriadicCube d) : TopologicalSpace.SeparableSpace ↥(canonicalAEEMuCorrectionSpaceData Q).correctionSpace

noncomputable def HCPolySupport.canonicalAEEMuCoeffOperatorData {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) : AEEMuCoeffOperatorData (cubeSet Q) ↑a

Canonical AEE coefficient-operator data on one quantitative AEE cube slice.

Equations

• HCPolySupport.canonicalAEEMuCoeffOperatorData Q k a = HCPolySupport.AEEMuCoeffOperatorData.ofIsAEEllipticFieldOn ⋯ ⋯

noncomputable def HCPolySupport.canonicalAEEMuOperatorSystemData {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) : AEEMuOperatorSystemData (cubeSet Q) ↑a

Canonical AEE doubled operator system on one quantitative AEE cube slice.

Equations

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

@[simp]

theorem HCPolySupport.correctionSpace_canonicalAEEMuOperatorSystemData {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) : (canonicalAEEMuOperatorSystemData Q k a).correctionSpace = canonicalAEEMuCorrectionSpaceData Q

@[simp]

theorem HCPolySupport.coeffOperatorData_canonicalAEEMuOperatorSystemData {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) : (canonicalAEEMuOperatorSystemData Q k a).coeffOperatorData = canonicalAEEMuCoeffOperatorData Q k a

theorem HCPolySupport.canonicalAEEMuOperatorSystemData_energyBilin_generator_eq_blockPairingAverage {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (Y Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) : ((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Y)) ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Z) = blockPairingAverage (cubeSet Q) (↑a) (canonicalMuGeneratorAffineField 0 Z) (canonicalMuGeneratorAffineField 0 Y)

The canonical AEE Hilbert bilinear form on dense generator corrections is the fixed block-pairing average of their chosen pointwise representatives.

theorem HCPolySupport.canonicalAEEMuOperatorSystemData_energyBilin_const_generator_eq_blockPairingAverage {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) : ((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin ((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.constantField P)) ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Y) = blockPairingAverage (cubeSet Q) (↑a) (canonicalMuGeneratorAffineField 0 Y) (canonicalMuGeneratorAffineField P 0)

The canonical AEE Hilbert bilinear form on a constant affine shift and a dense-generator correction is the fixed block-pairing average of their chosen pointwise representatives.

theorem HCPolySupport.mu_eq_canonicalAEEMuCandidate {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P0 : BlockVec d) : Mu (cubeSet Q) P0 ↑a = (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.muCandidate P0

The variational Mu on a quantitative AEE cube slice agrees with the canonical AEE Hilbert-operator candidate.

theorem HCPolySupport.mu_eq_iInf_blockEnergyAverage_canonicalAEEMuGenerator_denseSeq {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P0 : BlockVec d) (ξ : ℕ → ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) (hξ : DenseRange ξ) : Mu (cubeSet Q) P0 ↑a = ⨅ (n : ℕ), blockEnergyAverage (cubeSet Q) (↑a) (canonicalMuGeneratorAffineField P0 (ξ n))

On a quantitative AEE cube slice, the variational Mu is the infimum of the fixed-competitor block energies along any dense sequence in the canonical predicate-generated correction submodule. This is the canonical Ch4 bridge for Ch5 measurability: the competitors are pointwise block states and no external recovery witness is part of the interface.

theorem HCPolySupport.canonicalAEEMuOperatorSystemData_quadraticEnergy_generatorAffine_eq_blockEnergyAverage {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P0 : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) : have H := (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization; quadraticEnergy H.energyBilin (H.constantField P0 + ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Y)) = blockEnergyAverage (cubeSet Q) (↑a) (canonicalMuGeneratorAffineField P0 Y)

The Hilbert quadratic energy of a canonical dense-generator affine competitor is exactly its doubled block-energy average. This is the pointwise energy identity used by countable near-minimizer selections.

theorem HCPolySupport.mu_eq_iInf_blockEnergyAverage_canonicalAEEMuGenerator {d : ℕ} (Q : TriadicCube d) (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (P0 : BlockVec d) : Mu (cubeSet Q) P0 ↑a = ⨅ (n : ℕ), blockEnergyAverage (cubeSet Q) (↑a) (canonicalMuGeneratorAffineField P0 (TopologicalSpace.denseSeq (↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) n))

Canonical dense-sequence form of mu_eq_iInf_blockEnergyAverage_canonicalAEEMuGenerator_denseSeq, using TopologicalSpace.denseSeq on the canonical generator submodule.