Coarse-graining support: Support.CoarseGraining.MuOperator.AEEOperator.CoeffOperatorData

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

A.e.-elliptic coefficient-operator realization data

This file begins the Chapter 4 Phase 3 replacement for the pointwise MuOperatorSystemData handoff. The old deterministic package is built from pointwise IsEllipticFieldOn; the manuscript-facing support data is only spatial-a.e. elliptic. The structures below therefore store a measurable operator representative together with its a.e. agreement with the raw normalized coefficient operator.

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

Measurable representative data for the normalized doubled coefficient operator when the coefficient field is controlled only up to spatial null sets.

The pointwise field is the object used to build the L² operator. The ae_eq_normalizedBlockCoeffOperator field records that this representative is the same as the raw Ch4 coefficient operator on the observation set, modulo the restricted volume measure.

• measurableSet_domain : MeasurableSet U

  Measurability of the underlying domain.

• field : Vec d → HilbertBlockVec d →L[ℝ] HilbertBlockVec d

  A measurable representative of the normalized coefficient operator.

• measurable_field : Measurable self.field

  Measurability of the representative operator field.

• ae_eq_normalizedBlockCoeffOperator : self.field =ᵐ[volumeMeasureOn U] normalizedBlockCoeffOperator U a

  The representative agrees a.e. with the raw normalized coefficient operator.

• opNormBound : ℝ

  A uniform operator-norm bound for the representative.

• opNormBound_nonneg : 0 ≤ self.opNormBound

  Nonnegativity of the bound.

• le_opNormBound (x : Vec d) : ‖self.field x‖ ≤ self.opNormBound

  The representative operators are bounded by opNormBound.

• coercivityConstant : ℝ

  Coercivity constant for the induced L² operator.

• coercivityConstant_pos : 0 < self.coercivityConstant

  Positivity of the coercivity constant.

• ae_field_inner_comm : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ∀ (X Y : HilbertBlockVec d), inner ℝ ((self.field x) X) Y = inner ℝ X ((self.field x) Y)

  A.e. symmetry of the pointwise representative.

• ae_field_self_inner_lowerBound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ∀ (X : HilbertBlockVec d), self.coercivityConstant * inner ℝ X X ≤ inner ℝ ((self.field x) X) X

  A.e. pointwise coercivity of the representative.

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

Forget the a.e. identification data and keep the measurable bounded representative as a pointwise operator field.

Equations

• M.toPointwiseField = { field := M.field, measurable_field := ⋯, opNormBound := M.opNormBound, opNormBound_nonneg := ⋯, le_opNormBound := ⋯ }

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

The bounded L² operator induced by the measurable representative.

Equations

• M.operator = M.toPointwiseField.toContinuousLinearMap

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

Pointwise a.e. description of the representative-induced L² operator.

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

The representative-induced L² operator agrees a.e. with the raw normalized coefficient operator applied to F.

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

Symmetry of the L² operator induced by the a.e.-symmetric representative.

theorem HCPolySupport.AEEMuCoeffOperatorData.operatorCoercive {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : AEEMuCoeffOperatorData U a) : IsCoercive (energyBilinOfOperator M.operator)

Coercivity of the L² operator induced by the a.e.-coercive representative.

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

Package the a.e.-representative data as the concrete Mu operator realization expected by the Hilbert minimization layer.

Equations

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

theorem HCPolySupport.AEEMuCoeffOperatorData.le_normalizedBlockCoeffOperatorNormBound_of_isEllipticMatrix_of_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} {x : Vec d} (hx : x ∈ U) (hmat : IsEllipticMatrix lam Lam (a x)) : ‖normalizedBlockCoeffOperator U a x‖ ≤ MuCoeffOperatorData.normalizedBlockCoeffOperatorNormBound U lam Lam

theorem HCPolySupport.AEEMuCoeffOperatorData.measurable_normalizedBlockMatrixOperator {d : ℕ} {U : Set (Vec d)} (A : Vec d → Mat d) (hA_meas : Measurable A) : Measurable fun (x : Vec d) => (MeasureTheory.volume U).toReal⁻¹ • HilbertBlockVec.applyBlockMat (blockMatrixOfCoeff (A x))

Normalization preserves measurability of the associated block operator.

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

noncomputable def HCPolySupport.AEEMuCoeffOperatorData.ofIsAEEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsAEEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) : AEEMuCoeffOperatorData U a

Build a.e.-representative coefficient-operator data from spatial-a.e. ellipticity on U. The representative is obtained coordinatewise from AEStronglyMeasurable.mk, then clamped to the deterministic ellipticity norm bound; the clamping is invisible a.e. on the elliptic support.

Equations

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

noncomputable def HCPolySupport.AEEMuCoeffOperatorData.ofMuCoeffOperatorDataOfIsEllipticFieldOn {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) : AEEMuCoeffOperatorData U a

The old pointwise deterministic coefficient-operator data embeds in the new a.e.-representative package.

Equations

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

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

A.e.-representative operator-system data for the doubled \mu problem on U.

This is the Phase 3 target API: it has the same Hilbert-minimization output as MuOperatorSystemData, but its coefficient operator is allowed to be a measurable representative of the raw coefficient field.

• correctionSpace : MuCorrectionSpaceData U

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

• coeffOperatorData : AEEMuCoeffOperatorData U a

  A.e.-representative coefficient-operator data.

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

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

Equations

• M.toMuOperatorRealization = M.coeffOperatorData.toMuOperatorRealization

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

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

Equations

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

theorem HCPolySupport.MuHilbertRealization.muCandidate_eq_sInf_quadraticEnergy_correctionSpace {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (H : MuHilbertRealization U a) (P : BlockVec d) : H.muCandidate P = sInf (Set.range fun (Y : ↥↑H.correctionSpace.correctionSpace) => quadraticEnergy H.energyBilin (H.constantField P + ↑Y))

The Hilbert minimizer value is the infimum of the quadratic energy over the whole affine correction space.

theorem HCPolySupport.MuHilbertRealization.muCandidate_eq_sInf_quadraticEnergy_denseRange {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (H : MuHilbertRealization U a) (P : BlockVec d) {β : Type u_1} [Nonempty β] (g : β → ↥↑H.correctionSpace.correctionSpace) (hg : DenseRange g) : H.muCandidate P = sInf (Set.range fun (Y : β) => quadraticEnergy H.energyBilin (H.constantField P + ↑(g Y)))

Dense correction-space subsets may be used to compute the Hilbert minimizer value.

noncomputable def HCPolySupport.PotentialSolenoidalL2Data.submoduleClosureToMuCorrectionSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : ↥↑M.blockPotentialZeroTraceSolenoidalZeroNormalTrace → ↥↑M.toMuCorrectionSpaceData.correctionSpace

Transport an element of the closed block correction space into the Hilbert correction space.

Equations

• M.submoduleClosureToMuCorrectionSpace X = ⟨HCPolySupport.blockL2ToHilbertBlockL2 ↑X, ⋯⟩

theorem HCPolySupport.PotentialSolenoidalL2Data.continuous_submoduleClosureToMuCorrectionSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : Continuous M.submoduleClosureToMuCorrectionSpace

theorem HCPolySupport.PotentialSolenoidalL2Data.surjective_submoduleClosureToMuCorrectionSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : Function.Surjective M.submoduleClosureToMuCorrectionSpace

@[reducible, inline]

abbrev HCPolySupport.canonicalMuBlockCorrectionGeneratorSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(BlockL2 U)

The predicate-generated block correction submodule before topological closure.

Equations

• HCPolySupport.canonicalMuBlockCorrectionGeneratorSubmodule U = HCPolySupport.PotentialSolenoidalL2Data.blockPotentialZeroTraceSolenoidalZeroNormalTraceSubmodule U

noncomputable def HCPolySupport.canonicalMuCorrectionGeneratorEmbedding {d : ℕ} (U : Set (Vec d)) : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U) → ↥↑(MuCorrectionSpaceData.ofSubmoduleClosures U).correctionSpace

Embed predicate-generated block corrections into the canonical Hilbert correction space.

Equations

• HCPolySupport.canonicalMuCorrectionGeneratorEmbedding U Y = (HCPolySupport.PotentialSolenoidalL2Data.ofSubmoduleClosures U).submoduleClosureToMuCorrectionSpace ⟨↑Y, ⋯⟩

theorem HCPolySupport.denseRange_canonicalMuCorrectionGeneratorEmbedding {d : ℕ} (U : Set (Vec d)) : DenseRange (canonicalMuCorrectionGeneratorEmbedding U)

structure HCPolySupport.CanonicalMuGeneratorRepresentativeData {d : ℕ} (U : Set (Vec d)) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : Type

A pointwise representative for one predicate-generated canonical block correction. This is intentionally weaker than full recovery data: it only chooses representatives for the dense generating submodule, not for every element of the closed correction space.

• correction : CorrectionFieldData U

  Pointwise potential and flux correction representing the canonical dense generator Y in L².

• toBlockL2_eq : self.correction.toBlockL2 = ↑Y

noncomputable def HCPolySupport.canonicalMuGeneratorRepresentative {d : ℕ} {U : Set (Vec d)} (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : CanonicalMuGeneratorRepresentativeData U Y

Choose a pointwise representative for a canonical dense-generator correction.

Equations

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

noncomputable def HCPolySupport.canonicalMuGeneratorCorrectionFieldData {d : ℕ} {U : Set (Vec d)} (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : CorrectionFieldData U

The chosen generator representative as correction-field data.

Equations

• HCPolySupport.canonicalMuGeneratorCorrectionFieldData Y = (HCPolySupport.canonicalMuGeneratorRepresentative Y).correction

theorem HCPolySupport.canonicalMuGeneratorCorrectionFieldData_toBlockL2 {d : ℕ} {U : Set (Vec d)} (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : (canonicalMuGeneratorCorrectionFieldData Y).toBlockL2 = ↑Y

theorem HCPolySupport.canonicalMuCorrectionGeneratorEmbedding_eq_toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : ↑(canonicalMuCorrectionGeneratorEmbedding U Y) = (canonicalMuGeneratorCorrectionFieldData Y).toHilbertBlockL2

@[simp]

theorem HCPolySupport.canonicalMuCorrectionGeneratorEmbedding_zero {d : ℕ} {U : Set (Vec d)} : canonicalMuCorrectionGeneratorEmbedding U 0 = 0

noncomputable def HCPolySupport.canonicalMuGeneratorAffineField {d : ℕ} {U : Set (Vec d)} (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : BlockState d

The affine block state associated to a dense-generator correction.

Equations

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

theorem HCPolySupport.canonicalMuGeneratorAffineField_admissible {d : ℕ} {U : Set (Vec d)} (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : IsBlockMuAdmissible U P (canonicalMuGeneratorAffineField P Y)

theorem HCPolySupport.canonicalMuGeneratorAffineField_memBlockL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : MemBlockL2 U (canonicalMuGeneratorAffineField P Y).eval

theorem HCPolySupport.canonicalMuGeneratorAffineField_correction_eq {d : ℕ} {U : Set (Vec d)} (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : ⋯.toCorrectionFieldDataOfAdmissible.toHilbertBlockL2 = (canonicalMuGeneratorCorrectionFieldData Y).toHilbertBlockL2

theorem HCPolySupport.canonicalMuGeneratorAffineField_hilbert_eq_const_add {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (P : BlockVec d) (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : toHilbertBlockL2OfBlockField ⋯ = blockVecToHilbertBlockL2Const P + ↑(canonicalMuCorrectionGeneratorEmbedding U Y)

theorem HCPolySupport.canonicalMuGeneratorAffineField_zero_hilbert_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : toHilbertBlockL2OfBlockField ⋯ = ↑(canonicalMuCorrectionGeneratorEmbedding U Y)

theorem HCPolySupport.canonicalMuGeneratorAffineField_zeroCorrection_hilbert_eq_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (P : BlockVec d) : toHilbertBlockL2OfBlockField ⋯ = blockVecToHilbertBlockL2Const P

theorem HCPolySupport.continuous_canonicalMuCorrectionGeneratorEmbedding {d : ℕ} (U : Set (Vec d)) : Continuous (canonicalMuCorrectionGeneratorEmbedding U)

instance HCPolySupport.canonicalMuBlockCorrectionGeneratorSubmodule_separable {d : ℕ} (U : Set (Vec d)) : TopologicalSpace.SeparableSpace ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)