Coarse-graining support: Support.CoarseGraining.MuRecovery.Setup

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

Mu recovery -- private volume / bounded-domain helpers and data package

Volume positivity / finite lemmas on origin cubes and the MuMinimizerRecoveryData structure used as the interface between the Hilbert minimizer map and the note-faithful linear family.

theorem HCPolySupport.volume_cubeSet_originCube_lt_top_recovery {d : ℕ} (n : ℤ) : MeasureTheory.volume (cubeSet (originCube d n)) < ⊤

theorem HCPolySupport.volume_openCubeSet_originCube_lt_top_recovery {d : ℕ} (n : ℤ) : MeasureTheory.volume (openCubeSet (originCube d n)) < ⊤

theorem HCPolySupport.volume_cubeSet_originCube_toReal_pos_recovery {d : ℕ} (n : ℤ) : 0 < (MeasureTheory.volume (cubeSet (originCube d n))).toReal

theorem HCPolySupport.volume_openCubeSet_originCube_toReal_pos_recovery {d : ℕ} (n : ℤ) : 0 < (MeasureTheory.volume (openCubeSet (originCube d n))).toReal

theorem HCPolySupport.isBoundedDomain_openCubeSet_originCube_recovery {d : ℕ} (n : ℤ) : IsBoundedDomain (openCubeSet (originCube d n))

theorem HCPolySupport.isBoundedDomain_cubeSet_originCube_recovery {d : ℕ} (n : ℤ) : IsBoundedDomain (cubeSet (originCube d n))

theorem HCPolySupport.isSobolevRegularDomain_openCubeSet_originCube_recovery {d : ℕ} (n : ℤ) : IsSobolevRegularDomain (openCubeSet (originCube d n))

theorem HCPolySupport.isSobolevRegularDomain_cubeSet_originCube_recovery {d : ℕ} (n : ℤ) : IsSobolevRegularDomain (cubeSet (originCube d n))

This file isolates the remaining bridge from the Hilbert-space doubled \mu problem back to the note-faithful pointwise minimizer family.

The analytic minimization engine already produces a canonical linear map P ↦ X_P in the ambient Hilbert space L²(U; \R^{2d}). To recover the coarse-grained block matrix \mathbf A(U; a) from \mu(U, \cdot; a), the remaining missing input is a representative-level package asserting that these Hilbert minimizers come from actual block states with the expected admissibility and energy identities.

structure HCPolySupport.MuMinimizerRecoveryData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : Type

Representative-level recovery data for the Hilbert minimizers of the doubled \mu problem.

This package is intentionally theorem-surface only: it records the exact pointwise witnesses still needed to convert the Hilbert minimizer map into the note-faithful linear minimizer family used to prove \exists \mathbf A(U; a).

• system : MuOperatorSystemData U a

  The deterministic doubled operator package.

• field : BlockVec d → BlockState d

  A pointwise block-state representative of the Hilbert minimizer.

• map_add (P Q : BlockVec d) : self.field (P + Q) = self.field P + self.field Q

  Linearity in the coarse datum.

• map_smul (c : ℝ) (P : BlockVec d) : self.field (c • P) = c • self.field P

  Homogeneity in the coarse datum.

• mem_blockL2 (P : BlockVec d) : MemBlockL2 U (self.field P).eval

  Each representative is an actual block L² field.

• minimizer_eq (P : BlockVec d) : toHilbertBlockL2OfBlockField ⋯ = self.system.toMuHilbertRealization.minimizerMap P

  The chosen representative agrees with the Hilbert minimizer in L².

• admissible (P : BlockVec d) : IsBlockMuAdmissible U P (self.field P)

  The representative is admissible for the note's definition of \mu.

• pairingIntegrable (P Q : BlockVec d) : MeasureTheory.IntegrableOn (blockPairingIntegrand a (self.field P) (self.field Q)) U MeasureTheory.volume

  Pairing integrability needed for the quadratic-family API.

• mu_eq_muCandidate (P : BlockVec d) : Mu U P a = self.system.toMuHilbertRealization.muCandidate P

  The note's \mu agrees with the Hilbert-space minimized energy.