Coarse-graining support: Support.CoarseGraining.OriginCubeOpenBridge #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Deterministic origin-cube open/closed bridge #
This file keeps the deterministic cube/open-cube equivalences needed by Chapter 2 and coarse-graining. The old probability-facing annealed wrappers around these facts live only in the legacy probability archive.
Deterministic bridge data from the half-open origin cube to the corresponding
open cube at scale n.
This isolates the only genuinely domain-sensitive missing theorem needed to transport the Chapter-4 symmetry argument from the literally invariant open cube back to the currently defined half-open at-scale objects.
- coarseBlockMatrix_eq (a : CoeffField d) : coarseBlockMatrix (cubeSet (originCube d n)) a = coarseBlockMatrix (openCubeSet (originCube d n)) a
Instances For
theorem
HCPolySupport.volumeAverage_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
(n : ℤ)
(f : Vec d → ℝ)
:
theorem
HCPolySupport.responseJValueSet_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(p q : Vec d)
(a : CoeffField d)
:
responseJValueSet (cubeSet (originCube d n)) p q a = responseJValueSet (openCubeSet (originCube d n)) p q a
theorem
HCPolySupport.ResponseJ_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(p q : Vec d)
(a : CoeffField d)
:
theorem
HCPolySupport.responseJ_cubeSet_eq_openCubeSet_of_triadicCube
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(p q : Vec d)
(a : CoeffField d)
:
theorem
HCPolySupport.isBlockMuAdmissible_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{n : ℤ}
{P : BlockVec d}
{X : BlockState d}
:
IsBlockMuAdmissible (cubeSet (originCube d n)) P X ↔ IsBlockMuAdmissible (openCubeSet (originCube d n)) P X
theorem
HCPolySupport.isBlockMuAdmissible_cubeSet_triadicCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{P : BlockVec d}
{X : BlockState d}
:
Arbitrary-triadic-cube version of the open/half-open admissibility bridge
for the doubled Mu problem.
theorem
HCPolySupport.muValueSet_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(P : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.Mu_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(P : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.blockResponseSpace_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{X : BlockState d}
:
BlockResponseSpace a (cubeSet (originCube d n)) X ↔ BlockResponseSpace a (openCubeSet (originCube d n)) X
theorem
HCPolySupport.blockResponseIntegrabilityData_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
{n : ℤ}
{a : CoeffField d}
{X : BlockState d}
:
BlockResponseIntegrabilityData (cubeSet (originCube d n)) a X ↔ BlockResponseIntegrabilityData (openCubeSet (originCube d n)) a X
theorem
HCPolySupport.blockJValueSet_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(P Q : BlockVec d)
(a : CoeffField d)
:
blockJValueSet (cubeSet (originCube d n)) P Q a = blockJValueSet (openCubeSet (originCube d n)) P Q a
theorem
HCPolySupport.BlockJ_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(P Q : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.Mu_cubeSet_eq_openCubeSet_of_triadicCube
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(P : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.BlockJ_cubeSet_eq_openCubeSet_of_triadicCube
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(P Q' : BlockVec d)
(a : CoeffField d)
:
theorem
HCPolySupport.hasQuadraticMu_cubeSet_iff_openCubeSet_of_triadicCube
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
{a : CoeffField d}
:
theorem
HCPolySupport.coarseBlockMatrix_cubeSet_originCube_eq_openCubeSet
{d : ℕ}
[NeZero d]
(n : ℤ)
(a : CoeffField d)
:
theorem
HCPolySupport.isSigmaStarCoarse_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar : Mat d}
:
IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar ↔ IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar
theorem
HCPolySupport.isKappaCoarse_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
:
IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa ↔ IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa
theorem
HCPolySupport.isSigmaCoarse_cubeSet_originCube_iff_openCubeSet
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
:
IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa ↔ IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa
theorem
HCPolySupport.sigmaStarInvCoarse_cubeSet_originCube_eq_openCubeSet_of_isSigmaStarCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
:
sigmaStarInvCoarse (cubeSet (originCube d n)) a = sigmaStarInvCoarse (openCubeSet (originCube d n)) a
theorem
HCPolySupport.sigmaStarCoarse_cubeSet_originCube_eq_openCubeSet_of_isSigmaStarCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.sigmaStarInvKappaCoarse_cubeSet_originCube_eq_openCubeSet_of_isKappaCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
:
sigmaStarInvKappaCoarse (cubeSet (originCube d n)) a = sigmaStarInvKappaCoarse (openCubeSet (originCube d n)) a
theorem
HCPolySupport.kappaCoarse_cubeSet_originCube_eq_openCubeSet_of_isSigmaStarCoarse_and_isKappaCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.sigmaCorrectedResponse_cubeSet_originCube_eq_openCubeSet_of_isSigmaStarCoarse_and_isKappaCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(p : Vec d)
:
sigmaCorrectedResponse (cubeSet (originCube d n)) a p = sigmaCorrectedResponse (openCubeSet (originCube d n)) a p
theorem
HCPolySupport.sigmaCoarse_cubeSet_originCube_eq_openCubeSet_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
(hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.bCoarse_sigmaCoarse_sigmaStarCoarse_kappaCoarse_cubeSet_originCube_eq_openCubeSet_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
{n : ℤ}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse (cubeSet (originCube d n)) a sigmaStar)
(hK : IsKappaCoarse (cubeSet (originCube d n)) a sigmaStar kappa)
(hSigma : IsSigmaCoarse (cubeSet (originCube d n)) a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
:
bCoarse (sigmaCoarse (cubeSet (originCube d n)) a) (sigmaStarCoarse (cubeSet (originCube d n)) a)
(kappaCoarse (cubeSet (originCube d n)) a) = bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a)
(kappaCoarse (openCubeSet (originCube d n)) a)