Coarse-graining support: Support.CoarseGraining.MuAdmissibility

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

Admissibility-plus-integrability bridge lemmas for the doubled Mu problem.

IsBlockMuAdmissible U P X now packages the correction-field L² membership and the zero-trace / zero-normal-trace conditions. On finite-measure domains, this is enough to reconstruct the affine state as an ambient L² block field. Ellipticity then upgrades admissible states to the energy-integrability package needed for the quantitative averaged identities below.

structure HCPolySupport.BlockMuIntegrabilityData {d : ℕ} (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) (X : BlockState d) : Prop

L² integrability of both affine corrections and integrability of the block energy density on U.

• potentialCorrection_memL2 : MemVectorL2 U fun (x : Vec d) => X.potential x - P.1
• fluxCorrection_memL2 : MemVectorL2 U fun (x : Vec d) => X.flux x - P.2
• energyIntegrable : MeasureTheory.IntegrableOn (blockEnergyDensity a X) U MeasureTheory.volume

theorem HCPolySupport.blockMuIntegrabilityData_of_memBlockL2_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} (hX : MemBlockL2 U X.eval) (hEll : IsEllipticFieldOn lam Lam U a) : BlockMuIntegrabilityData U P a X

Ambient block L² control plus ellipticity is enough to build the integrability package used by the doubled Mu bridge.

noncomputable def HCPolySupport.IsBlockMuAdmissible.toCorrectionFieldDataOfAdmissible {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : CorrectionFieldData U

The correction field attached to an admissible block state depends only on the affine constraints packaged by IsBlockMuAdmissible.

Equations

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

noncomputable def HCPolySupport.IsBlockMuAdmissible.toCorrectionFieldData {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) (hInt : BlockMuIntegrabilityData U P a X) : CorrectionFieldData U

The admissible corrections X.potential - P.1 and X.flux - P.2, bundled with L² membership and zero-trace conditions.

Equations

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

@[simp]

theorem HCPolySupport.IsBlockMuAdmissible.toCorrectionFieldData_potential {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) (hInt : BlockMuIntegrabilityData U P a X) : (hX.toCorrectionFieldData hInt).potential = fun (x : Vec d) => X.potential x - P.1

@[simp]

theorem HCPolySupport.IsBlockMuAdmissible.toCorrectionFieldData_flux {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) (hInt : BlockMuIntegrabilityData U P a X) : (hX.toCorrectionFieldData hInt).flux = fun (x : Vec d) => X.flux x - P.2

theorem HCPolySupport.IsBlockMuAdmissible.memBlockL2_eval {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hX : IsBlockMuAdmissible U P X) : MemBlockL2 U X.eval

Reconstruct the ambient block L² field carried by an admissible state.

theorem HCPolySupport.IsBlockMuAdmissible.toCorrectionFieldData_mem_correctionSpace {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : hX.toCorrectionFieldDataOfAdmissible.toHilbertBlockL2 ∈ (PotentialSolenoidalL2Data.ofSubmoduleClosures U).toMuCorrectionSpaceData.correctionSpace

The admissible correction carried by X lands in the canonical closed correction space \Lpoto(U) × \Lsolo(U).

theorem HCPolySupport.IsBlockMuAdmissible.toHilbertBlockL2OfBlockField_eq_blockVecToHilbertBlockL2Const_add {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hX : IsBlockMuAdmissible U P X) : toHilbertBlockL2OfBlockField ⋯ = blockVecToHilbertBlockL2Const P + hX.toCorrectionFieldDataOfAdmissible.toHilbertBlockL2

The Hilbert image of an admissible block state splits into the constant datum P plus its correction component.

noncomputable def HCPolySupport.IsBlockMuAdmissible.toCorrectionSpaceElement {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : ↥↑(PotentialSolenoidalL2Data.ofSubmoduleClosures U).toMuCorrectionSpaceData.correctionSpace

Package the correction component of an admissible state as an element of the canonical closed correction space.

Equations

• hX.toCorrectionSpaceElement = ⟨hX.toCorrectionFieldDataOfAdmissible.toHilbertBlockL2, ⋯⟩

theorem HCPolySupport.IsBlockMuAdmissible.toHilbertBlockL2OfBlockField_eq_blockVecToHilbertBlockL2Const_add_correctionSpace {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hX : IsBlockMuAdmissible U P X) : toHilbertBlockL2OfBlockField ⋯ = blockVecToHilbertBlockL2Const P + ↑hX.toCorrectionSpaceElement

theorem HCPolySupport.IsBlockMuAdmissible.toBlockMuIntegrabilityDataOfIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} (hX : IsBlockMuAdmissible U P X) (hEll : IsEllipticFieldOn lam Lam U a) : BlockMuIntegrabilityData U P a X

theorem HCPolySupport.IsBlockMuAdmissible.pairingIntegrable {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hX : IsBlockMuAdmissible U P X) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (X.potential x) (X.flux x)) U MeasureTheory.volume

theorem HCPolySupport.IsBlockMuAdmissible.average_pairing_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hX : IsBlockMuAdmissible U P X) (hpotZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.potential x - P.1) i) = 0) (hfluxZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.flux x - P.2) i) = 0) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : (volumeAverage U fun (x : Vec d) => vecDot (X.potential x) (X.flux x)) = vecDot P.1 P.2

theorem HCPolySupport.IsBlockMuAdmissible.blockEnergyAverage_ge_vecDot_of_integral_eq_zero_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} (hX : IsBlockMuAdmissible U P X) (hInt : BlockMuIntegrabilityData U P a X) (hEll : IsEllipticFieldOn lam Lam U a) (hpotZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.potential x - P.1) i) = 0) (hfluxZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.flux x - P.2) i) = 0) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : vecDot P.1 P.2 ≤ blockEnergyAverage U a X

theorem HCPolySupport.IsBlockMuAdmissible.mu_ge_vecDot_of_isEllipticFieldOn_of_integrabilityBridge {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (bridge : ∀ (X : BlockState d), IsBlockMuAdmissible U P X → BlockMuIntegrabilityData U P a X) (hpotZero : ∀ (X : BlockState d), IsBlockMuAdmissible U P X → (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.potential x - P.1) i) = 0) (hfluxZero : ∀ (X : BlockState d), IsBlockMuAdmissible U P X → (fun (i : Fin d) => ∫ (x : Vec d) in U, (X.flux x - P.2) i) = 0) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : vecDot P.1 P.2 ≤ Mu U P a

theorem HCPolySupport.IsBlockMuAdmissible.mu_ge_vecDot_of_isEllipticFieldOn_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) : vecDot P.1 P.2 ≤ Mu U P a

theorem HCPolySupport.IsBlockMuAdmissible.average_pairing_openCubeSet_originCube {d : ℕ} {n : ℤ} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible (openCubeSet (originCube d n)) P X) : (volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => vecDot (X.potential x) (X.flux x)) = vecDot P.1 P.2

theorem HCPolySupport.IsBlockMuAdmissible.average_pairing_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible (cubeSet (originCube d n)) P X) : (volumeAverage (cubeSet (originCube d n)) fun (x : Vec d) => vecDot (X.potential x) (X.flux x)) = vecDot P.1 P.2

theorem HCPolySupport.IsBlockMuAdmissible.blockEnergyAverage_ge_vecDot_openCubeSet_originCube_of_isEllipticFieldOn {d : ℕ} {n : ℤ} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} {lam Lam : ℝ} (hX : IsBlockMuAdmissible (openCubeSet (originCube d n)) P X) (hInt : BlockMuIntegrabilityData (openCubeSet (originCube d n)) P a X) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) : vecDot P.1 P.2 ≤ blockEnergyAverage (openCubeSet (originCube d n)) a X

theorem HCPolySupport.IsBlockMuAdmissible.blockEnergyAverage_ge_vecDot_cubeSet_originCube_of_isEllipticFieldOn {d : ℕ} [NeZero d] {n : ℤ} {P : BlockVec d} {a : CoeffField d} {X : BlockState d} {lam Lam : ℝ} (hX : IsBlockMuAdmissible (cubeSet (originCube d n)) P X) (hInt : BlockMuIntegrabilityData (cubeSet (originCube d n)) P a X) (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) : vecDot P.1 P.2 ≤ blockEnergyAverage (cubeSet (originCube d n)) a X

theorem HCPolySupport.IsBlockMuAdmissible.mu_ge_vecDot_openCubeSet_originCube_of_isEllipticFieldOn_of_integrabilityBridge {d : ℕ} {n : ℤ} {P : BlockVec d} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (bridge : ∀ (Y : BlockState d), IsBlockMuAdmissible (openCubeSet (originCube d n)) P Y → BlockMuIntegrabilityData (openCubeSet (originCube d n)) P a Y) : vecDot P.1 P.2 ≤ Mu (openCubeSet (originCube d n)) P a

theorem HCPolySupport.IsBlockMuAdmissible.mu_ge_vecDot_cubeSet_originCube_of_isEllipticFieldOn_of_integrabilityBridge {d : ℕ} [NeZero d] {n : ℤ} {P : BlockVec d} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet (originCube d n)) a) (bridge : ∀ (Y : BlockState d), IsBlockMuAdmissible (cubeSet (originCube d n)) P Y → BlockMuIntegrabilityData (cubeSet (originCube d n)) P a Y) : vecDot P.1 P.2 ≤ Mu (cubeSet (originCube d n)) P a