Coarse-graining support: Support.CoarseGraining.MuOperator.CoeffOperator

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

Mu operator -- coefficient-operator realization and system APIs

MuCoeffOperatorData structure and namespace with measurability, uniform-bound, operator / operatorSymm / operatorCoercive constructors under IsEllipticFieldOn, the blockPairing / blockEnergy integrability lemmas, and the MuOperatorRealization / MuOperatorSystemData / PotentialSolenoidalL2Data namespaces that feed into the Mu-recovery layer.

structure HCPolySupport.MuCoeffOperatorData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

Measurability and uniform boundedness package for the normalized doubled coefficient operator attached to a.

This is the remaining analytic input needed to turn x ↦ \mathbf A(a,x) into a concrete MuOperatorRealization U a.

• measurableSet_domain : MeasurableSet U

  Measurability of the underlying domain.

• measurable_normalizedBlockCoeffOperator : Measurable (normalizedBlockCoeffOperator U a)

  Measurability of the normalized pointwise coefficient operator.

• opNormBound : ℝ

  A uniform operator-norm bound.

• opNormBound_nonneg : 0 ≤ self.opNormBound

  Nonnegativity of the bound.

• le_opNormBound (x : Vec d) : ‖normalizedBlockCoeffOperator U a x‖ ≤ self.opNormBound

  The normalized coefficient operators are bounded by opNormBound.

noncomputable def HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperatorNormBound {d : ℕ} (U : Set (Vec d)) (lam Lam : ℝ) : ℝ

The square root of the block matrix squared norm bound, divided by the real volume of U.

Equations

• HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperatorNormBound U lam Lam = (MeasureTheory.volume U).toReal⁻¹ * √(HCPolySupport.blockMatrixOfCoeffNormSqBound lam Lam)

theorem HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperatorNormBound_nonneg {d : ℕ} (U : Set (Vec d)) (lam Lam : ℝ) : 0 ≤ normalizedBlockCoeffOperatorNormBound U lam Lam

theorem HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperator_eq_of_mem {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {x : Vec d} (hx : x ∈ U) : normalizedBlockCoeffOperator U a x = (MeasureTheory.volume U).toReal⁻¹ • HilbertBlockVec.applyBlockMat (blockCoeffField a x)

theorem HCPolySupport.MuCoeffOperatorData.measurable_normalizedBlockCoeffOperator_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : Measurable (normalizedBlockCoeffOperator U a)

theorem HCPolySupport.MuCoeffOperatorData.le_normalizedBlockCoeffOperatorNormBound_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (x : Vec d) : ‖normalizedBlockCoeffOperator U a x‖ ≤ normalizedBlockCoeffOperatorNormBound U lam Lam

noncomputable def HCPolySupport.MuCoeffOperatorData.ofIsEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : MuCoeffOperatorData U a

Concrete measurable/bounded coefficient-operator data built directly from the ellipticity assumptions recorded in IsEllipticFieldOn.

Equations

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

noncomputable def HCPolySupport.MuCoeffOperatorData.toPointwiseField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) : PointwiseHilbertBlockOperatorField U

View the normalized coefficient operator as a uniformly bounded measurable pointwise L² operator field.

Equations

• M.toPointwiseField = { field := HCPolySupport.normalizedBlockCoeffOperator U a, measurable_field := ⋯, opNormBound := M.opNormBound, opNormBound_nonneg := ⋯, le_opNormBound := ⋯ }

noncomputable def HCPolySupport.MuCoeffOperatorData.operator {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)

The bounded L² operator induced by the normalized coefficient field.

Equations

• M.operator = M.toPointwiseField.toContinuousLinearMap

theorem HCPolySupport.MuCoeffOperatorData.ae_apply_operator {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) (F : ↥(HilbertBlockL2 U)) : ↑↑(M.operator F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (normalizedBlockCoeffOperator U a x) (↑↑F x)

theorem HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperator_inner_comm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (x : Vec d) (X Y : HilbertBlockVec d) : inner ℝ ((normalizedBlockCoeffOperator U a x) X) Y = inner ℝ X ((normalizedBlockCoeffOperator U a x) Y)

theorem HCPolySupport.MuCoeffOperatorData.normalizedBlockCoeffOperator_self_inner_lowerBound_of_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) {x : Vec d} (hx : x ∈ U) (X : HilbertBlockVec d) : (MeasureTheory.volume U).toReal⁻¹ * (lam / (1 + 2 * Lam ^ 2)) * inner ℝ X X ≤ inner ℝ ((normalizedBlockCoeffOperator U a x) X) X

theorem HCPolySupport.MuCoeffOperatorData.nonempty_of_volume_toReal_pos {d : ℕ} {U : Set (Vec d)} (hvol : 0 < (MeasureTheory.volume U).toReal) : U.Nonempty

theorem HCPolySupport.MuCoeffOperatorData.lam_pos_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : 0 < lam

theorem HCPolySupport.MuCoeffOperatorData.operatorSymm {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) : (↑M.operator).IsSymmetric

theorem HCPolySupport.MuCoeffOperatorData.operatorCoercive_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : IsCoercive (energyBilinOfOperator M.operator)

noncomputable def HCPolySupport.rawBlockCoeffOperatorField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : PointwiseHilbertBlockOperatorField U

The unnormalized pointwise doubled coefficient operator attached to a, viewed as a bounded measurable operator field on the Hilbert block carrier.

This auxiliary field is used only to prove integrability of the raw pairing X · A(a,x) Y from block L² control and ellipticity.

Equations

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

theorem HCPolySupport.blockPairingIntegrand_integrableOn_of_memBlockL2_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {X Y : BlockState d} (hX : MemBlockL2 U X.eval) (hY : MemBlockL2 U Y.eval) (hEll : IsEllipticFieldOn lam Lam U a) : MeasureTheory.IntegrableOn (blockPairingIntegrand a X Y) U MeasureTheory.volume

Ellipticity plus block L² control makes the raw doubled pairing integrable on U.

theorem HCPolySupport.blockEnergyDensity_integrableOn_of_memBlockL2_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {X : BlockState d} (hX : MemBlockL2 U X.eval) (hEll : IsEllipticFieldOn lam Lam U a) : MeasureTheory.IntegrableOn (blockEnergyDensity a X) U MeasureTheory.volume

Ellipticity plus block L² control makes the raw doubled energy density integrable on U.

structure HCPolySupport.MuOperatorRealization {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

Concrete L²(U; \R^{2d}) data for the note's averaged doubled coefficient operator.

The field ae_apply says that the operator acts pointwise by the doubled block matrix \mathbf A(a,x), multiplied by the normalizing factor appearing in \fint_U.

• operator : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)

  The ambient L² operator.

• ae_apply (F : ↥(HilbertBlockL2 U)) : ↑↑(self.operator F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (MeasureTheory.volume U).toReal⁻¹ • (HilbertBlockVec.applyBlockMat (blockCoeffField a x)) (↑↑F x)

  Almost-everywhere pointwise description of the averaged operator.

• operatorSymm : (↑self.operator).IsSymmetric

  Symmetry of the induced bilinear form.

• operatorCoercive : IsCoercive (energyBilinOfOperator self.operator)

  Coercivity of the induced bilinear form.

noncomputable def HCPolySupport.MuOperatorRealization.toMuHilbertRealization {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuOperatorRealization U a) (correctionSpace : MuCorrectionSpaceData U) : MuHilbertRealization U a

Forget the pointwise description and feed the operator package into the Hilbert-space \mu problem.

Equations

• M.toMuHilbertRealization correctionSpace = HCPolySupport.MuHilbertRealization.ofOperator correctionSpace M.operator ⋯ ⋯

theorem HCPolySupport.MuOperatorRealization.energyBilin_eq_volumeAverage_swap_of_memBlockL2 {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuOperatorRealization U a) {X Y : Vec d → BlockVec d} (hX : MemBlockL2 U X) (hY : MemBlockL2 U Y) : ((energyBilinOfOperator M.operator) (toHilbertBlockL2OfBlockField hY)) (toHilbertBlockL2OfBlockField hX) = volumeAverage U fun (x : Vec d) => blockVecDot (X x) (blockMatVecMul (blockCoeffField a x) (Y x))

For typed block L² fields, the Hilbert-space bilinear form of a concrete MuOperatorRealization reproduces the note's averaged doubled pairing.

The arguments appear in the order dictated by energyBilinOfOperator: the operator acts on the first entry. Writing the theorem with the fields swapped makes the right-hand side match the note's convention X \cdot \mathbf A(a,x) Y.

theorem HCPolySupport.MuOperatorRealization.energyBilin_eq_blockPairingAverage_of_blockState {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuOperatorRealization U a) {X Y : BlockState d} (hX : MemBlockL2 U X.eval) (hY : MemBlockL2 U Y.eval) : ((energyBilinOfOperator M.operator) (toHilbertBlockL2OfBlockField hY)) (toHilbertBlockL2OfBlockField hX) = blockPairingAverage U a X Y

theorem HCPolySupport.MuOperatorRealization.quadraticEnergy_eq_blockEnergyAverage_of_blockState {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuOperatorRealization U a) {X : BlockState d} (hX : MemBlockL2 U X.eval) : quadraticEnergy (energyBilinOfOperator M.operator) (toHilbertBlockL2OfBlockField hX) = blockEnergyAverage U a X

noncomputable def HCPolySupport.MuCoeffOperatorData.toMuOperatorRealization {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuCoeffOperatorData U a) (operatorSymm : (↑M.operator).IsSymmetric) (operatorCoercive : IsCoercive (energyBilinOfOperator M.operator)) : MuOperatorRealization U a

Package measurable bounded coefficient-operator data together with the symmetry and coercivity hypotheses needed by the doubled \mu problem.

Equations

• M.toMuOperatorRealization operatorSymm operatorCoercive = { operator := M.operator, ae_apply := ⋯, operatorSymm := operatorSymm, operatorCoercive := operatorCoercive }

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

Package measurable bounded coefficient-operator data into a concrete doubled operator realization using the symmetry and coercivity consequences of the ellipticity hypotheses.

Equations

• M.toMuOperatorRealizationOfIsEllipticFieldOn hEll hvol = M.toMuOperatorRealization ⋯ ⋯

structure HCPolySupport.MuOperatorSystemData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

Deterministic input data for the doubled \mu problem on U.

This bundles exactly the concrete operator-theoretic witnesses currently needed to pass from a coefficient field to the Hilbert-space minimization engine. The package is intentionally samplewise, so a future random-field layer can assign one such package to each realization \omega without changing the deterministic API.

• correctionSpace : MuCorrectionSpaceData U

  The closed correction space \Lpoto(U) × \Lsolo(U).

• coeffOperatorData : MuCoeffOperatorData U a

  Measurable bounded coefficient-operator data.

• operatorSymm : (↑self.coeffOperatorData.operator).IsSymmetric

  Symmetry of the concrete doubled L² operator.

• operatorCoercive : IsCoercive (energyBilinOfOperator self.coeffOperatorData.operator)

  Coercivity of the concrete doubled energy form.

noncomputable def HCPolySupport.MuOperatorSystemData.withCorrectionSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuOperatorSystemData U a) (correctionSpace : MuCorrectionSpaceData U) : MuOperatorSystemData U a

Replace the correction-space package while keeping the same coefficient operator data, symmetry, and coercivity witnesses.

Equations

• M.withCorrectionSpace correctionSpace = { correctionSpace := correctionSpace, coeffOperatorData := M.coeffOperatorData, operatorSymm := ⋯, operatorCoercive := ⋯ }

noncomputable def HCPolySupport.MuOperatorSystemData.toMuOperatorRealization {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuOperatorSystemData U a) : MuOperatorRealization U a

The concrete doubled operator realization extracted from the deterministic system package.

Equations

• M.toMuOperatorRealization = M.coeffOperatorData.toMuOperatorRealization ⋯ ⋯

noncomputable def HCPolySupport.MuOperatorSystemData.toMuHilbertRealization {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (M : MuOperatorSystemData U a) : MuHilbertRealization U a

The concrete Hilbert-space realization of the doubled \mu problem extracted from the deterministic system package.

Equations

• M.toMuHilbertRealization = M.toMuOperatorRealization.toMuHilbertRealization M.correctionSpace

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.toMuOperatorSystemData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : PotentialSolenoidalL2Data U) (coeffOperatorData : MuCoeffOperatorData U a) (operatorSymm : (↑coeffOperatorData.operator).IsSymmetric) (operatorCoercive : IsCoercive (energyBilinOfOperator coeffOperatorData.operator)) : MuOperatorSystemData U a

Build the deterministic doubled operator package directly from the packaged block correction space \Lpoto(U) × \Lsolo(U) together with the concrete coefficient-operator data.

Equations

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

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.toMuOperatorSystemDataOfIsEllipticFieldOn {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) : MuOperatorSystemData U a

Build the deterministic doubled operator system directly from a packaged potential/solenoidal correction space and raw ellipticity assumptions.

Equations

• M.toMuOperatorSystemDataOfIsEllipticFieldOn hEll hvol = M.toMuOperatorSystemData (HCPolySupport.MuCoeffOperatorData.ofIsEllipticFieldOn hEll) ⋯ ⋯

@[simp]

theorem HCPolySupport.PotentialSolenoidalL2Data.correctionSpace_toMuOperatorSystemData {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : PotentialSolenoidalL2Data U) (coeffOperatorData : MuCoeffOperatorData U a) (operatorSymm : (↑coeffOperatorData.operator).IsSymmetric) (operatorCoercive : IsCoercive (energyBilinOfOperator coeffOperatorData.operator)) : (M.toMuOperatorSystemData coeffOperatorData operatorSymm operatorCoercive).correctionSpace = M.toMuCorrectionSpaceData