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

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

Canonical solution-field measurability (carrier re-aim, Packet P5f)

This file re-aims the public Ch4 canonical doubled-Mu Hilbert-minimizer measurability surface onto the honest carrier RegCoeffField d, mirroring the Mu re-aim (Theorems/Mu.lean). The two per-slice primitives (minimizer strong measurability and fixed-test energy pairing) are re-derived Ω-generically through the L² realization in Internal/AEESliceAssembly/CarrierMinimizerFamily.lean.

The selected minimizer/energy-pairing observables are totalized with the least AEE quantitative slice index (else 0), so a genuine liftCover over the first-slice partition makes a ↦ observable a.toFun genuinely LocalSigmaR (cubeSet Q)-measurable on the whole carrier (a genuine-where-null strengthening: no a.e. bookkeeping is needed for these observables, unlike Mu). The honest bridge nullMeasurableSet_of_localSigmaR then promotes it, and the separable range of the slice-indexed minimizers upgrades to AEStronglyMeasurable.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalMuHilbertMinimizer_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertMinimizerCubeSet Q P0 a.toFun) P

Public Ch4 law-facing measurability of the selected canonical doubled-Mu Hilbert minimizer on a deterministic cube (carrier re-type).

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalMuHilbertPotential_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertPotentialCubeSet Q P0 a.toFun) P

Law-facing strong measurability of the potential component of the selected doubled-Mu Hilbert minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalMuHilbertFlux_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertFluxCubeSet Q P0 a.toFun) P

Law-facing strong measurability of the flux component of the selected doubled-Mu Hilbert minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalMuHilbertPotential_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertPotentialCubeSet Q P0 a.toFun) P

Law-facing a.e.-measurability of the potential component of the selected doubled-Mu Hilbert minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalMuHilbertFlux_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertFluxCubeSet Q P0 a.toFun) P

Law-facing a.e.-measurability of the flux component of the selected doubled-Mu Hilbert minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalDoubledMuResponsePotentialField_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponsePotentialFieldCubeSet Q p q a.toFun) P

Law-facing strong measurability of the selected doubled-Mu potential field.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalDoubledMuResponseFluxField_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseFluxFieldCubeSet Q p q a.toFun) P

Law-facing strong measurability of the selected doubled-Mu flux field.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponsePotentialField_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponsePotentialFieldCubeSet Q p q a.toFun) P

Law-facing a.e.-measurability of the selected doubled-Mu potential field.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseFluxField_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseFluxFieldCubeSet Q p q a.toFun) P

Law-facing a.e.-measurability of the selected doubled-Mu flux field.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponsePotentialFieldAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponsePotentialFieldAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of selected doubled-Mu potential averages over a deterministic subcube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseFluxFieldAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseFluxFieldAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of selected doubled-Mu flux averages over a deterministic subcube.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_descendantsAverageCanonicalDoubledMuResponsePotentialFieldAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => descendantsAverageCanonicalDoubledMuResponsePotentialFieldAverageCubeSet Q j p q a.toFun) P

Law-facing measurability of finite descendant averages of selected response-gradient averages.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_descendantsAverageCanonicalDoubledMuResponseFluxFieldAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => descendantsAverageCanonicalDoubledMuResponseFluxFieldAverageCubeSet Q j p q a.toFun) P

Law-facing measurability of finite descendant averages of selected response-flux averages.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponsePotentialWeakNormPartial_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (s : ℝ) (N : ℕ) (p q p0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponsePotentialWeakNormPartialCubeSet Q s N p q p0 a.toFun) P

Law-facing measurability of finite-depth selected response-gradient weak norms.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseFluxWeakNormPartial_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (t : ℝ) (N : ℕ) (p q q0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseFluxWeakNormPartialCubeSet Q t N p q q0 a.toFun) P

Law-facing measurability of finite-depth selected response-flux weak norms.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponsePotentialWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponsePotentialWeakNormCubeSet Q s p q p0 a.toFun) P

Law-facing measurability of the selected doubled-Mu potential weak norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseFluxWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (t : ℝ) (p q q0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseFluxWeakNormCubeSet Q t p q q0 a.toFun) P

Law-facing measurability of the selected doubled-Mu flux weak norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalMuHilbertEnergyBilinFixed_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) (Y : BlockState d) (hY : MemBlockL2 (cubeSet Q) Y.eval) : AEMeasurable (fun (a : RegCoeffField d) => canonicalMuHilbertEnergyBilinFixedCubeSet Q P0 Y hY a.toFun) P

Law-facing measurability of a fixed-test Hilbert energy pairing against the selected canonical doubled-Mu minimizer. This is the public Ch4 source for raw scalar-response operator-image averages.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseUpperImageAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseUpperImageAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of the upper coefficient-operator image averages of the selected doubled-Mu response minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalDoubledMuResponseLowerImageAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalDoubledMuResponseLowerImageAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of the lower coefficient-operator image averages of the selected doubled-Mu response minimizer.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseGradientAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseGradientAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of raw scalar response-gradient averages avg_R grad v_m.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseFluxAverage_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q R : TriadicCube d) (p q : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseFluxAverageCubeSet Q R p q a.toFun) P

Law-facing measurability of raw scalar response-flux averages avg_R a grad v_m.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseGradientWeakNormPartial_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (s : ℝ) (N : ℕ) (p q p0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseGradientWeakNormPartialCubeSet Q s N p q p0 a.toFun) P

Law-facing measurability of finite-depth raw scalar response-gradient weak norms.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseFluxWeakNormPartial_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (t : ℝ) (N : ℕ) (p q q0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseFluxWeakNormPartialCubeSet Q t N p q q0 a.toFun) P

Law-facing measurability of finite-depth raw scalar response-flux weak norms.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseGradientWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun) P

Law-facing measurability of the full raw scalar response-gradient weak norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_canonicalScalarResponseFluxWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (t : ℝ) (p q q0 : Vec d) : AEMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun) P

Law-facing measurability of the full raw scalar response-flux weak norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalScalarResponseGradientWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (s : ℝ) (p q p0 : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun) P

Law-facing strong measurability of the full raw scalar response-gradient weak norm.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_canonicalScalarResponseFluxWeakNorm_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (t : ℝ) (p q q0 : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun) P

Law-facing strong measurability of the full raw scalar response-flux weak norm.