Coarse-graining support: Support.Ambient.CoefficientFieldHilbert

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

@[instance_reducible]

def HCPolySupport.matMeasurableSpace {d : ℕ} : MeasurableSpace (Mat d)

The coordinatewise measurable structure on real d × d matrices.

Equations

• HCPolySupport.matMeasurableSpace = HCPolySupport.matMeasurableSpace._aux_1

theorem HCPolySupport.matBorelSpace {d : ℕ} : BorelSpace (Mat d)

@[instance_reducible]

noncomputable def HCPolySupport.hilbertVecOperatorMeasurableSpace {d : ℕ} : MeasurableSpace (HilbertVec d →L[ℝ] HilbertVec d)

The Borel measurable structure on continuous linear endomorphisms of the Euclidean Hilbert space.

Equations

• HCPolySupport.hilbertVecOperatorMeasurableSpace = borel (HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertVec d)

theorem HCPolySupport.hilbertVecOperatorBorelSpace {d : ℕ} : BorelSpace (HilbertVec d →L[ℝ] HilbertVec d)

noncomputable def HCPolySupport.matContinuousLinearMap {d : ℕ} (A : Mat d) : Vec d →L[ℝ] Vec d

A matrix acts continuously on the project's algebraic vector carrier.

Equations

• HCPolySupport.matContinuousLinearMap A = { toLinearMap := Matrix.toLin' A, cont := ⋯ }

@[simp]

theorem HCPolySupport.matContinuousLinearMap_apply {d : ℕ} (A : Mat d) (x : Vec d) : (matContinuousLinearMap A) x = matVecMul A x

noncomputable def HCPolySupport.HilbertVec.applyMat {d : ℕ} (A : Mat d) : HilbertVec d →L[ℝ] HilbertVec d

A matrix acts continuously on the Euclidean Hilbert realization of \R^d by conjugating the algebraic action through HilbertVec d ≃L[ℝ] Vec d.

Equations

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

@[simp]

theorem HCPolySupport.HilbertVec.applyMat_apply {d : ℕ} (A : Mat d) (x : HilbertVec d) : (applyMat A) x = ofVec (matVecMul A x.toVec)

@[simp]

theorem HCPolySupport.HilbertVec.applyMat_zero {d : ℕ} : applyMat 0 = 0

theorem HCPolySupport.HilbertVec.norm_sq_ofVec {d : ℕ} (x : Vec d) : ‖ofVec x‖ ^ 2 = vecDot x x

theorem HCPolySupport.HilbertVec.norm_sq_eq_vecDot {d : ℕ} (x : HilbertVec d) : ‖x‖ ^ 2 = vecDot x.toVec x.toVec

theorem HCPolySupport.HilbertVec.inner_ofVec_applyMat {d : ℕ} (A : Mat d) (x y : Vec d) : inner ℝ (ofVec x) ((applyMat A) (ofVec y)) = vecDot x (matVecMul A y)

theorem HCPolySupport.HilbertVec.norm_sq_applyMat {d : ℕ} (A : Mat d) (x : HilbertVec d) : ‖(applyMat A) x‖ ^ 2 = vecDot (matVecMul A x.toVec) (matVecMul A x.toVec)

theorem HCPolySupport.HilbertVec.opNorm_applyMat_le_of_vec_bound {d : ℕ} {A : Mat d} {C : ℝ} (hC : 0 ≤ C) (hA : ∀ (ξ : Vec d), vecDot (matVecMul A ξ) (matVecMul A ξ) ≤ C ^ 2 * vecDot ξ ξ) : ‖applyMat A‖ ≤ C

theorem HCPolySupport.HilbertVec.opNorm_applyMat_le_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : ‖applyMat A‖ ≤ Lam

structure HCPolySupport.PointwiseHilbertVecOperatorField {d : ℕ} (U : Set (Vec d)) : Type

Measurable uniformly bounded pointwise operator fields on the Hilbert-vector carrier over U.

This is the vector-side analogue of the doubled MuOperator infrastructure.

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

  The pointwise operator field.

• measurable_field : Measurable self.field

  Measurability of the operator field.

• opNormBound : ℝ

  A uniform operator-norm bound.

• opNormBound_nonneg : 0 ≤ self.opNormBound

  Nonnegativity of the bound.

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

  The pointwise operators are bounded by opNormBound.

noncomputable def HCPolySupport.PointwiseHilbertVecOperatorField.applyFn {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : Vec d → HilbertVec d

Pointwise action of the operator field on a typed L² vector field.

Equations

• M.applyFn F x = (M.field x) (↑↑F x)

theorem HCPolySupport.PointwiseHilbertVecOperatorField.aestronglyMeasurable_applyFn {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : MeasureTheory.AEStronglyMeasurable (M.applyFn F) (volumeMeasureOn U)

theorem HCPolySupport.PointwiseHilbertVecOperatorField.memHilbertVectorL2_applyFn {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : MemHilbertVectorL2 U (M.applyFn F)

noncomputable def HCPolySupport.PointwiseHilbertVecOperatorField.apply {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : ↥(HilbertVectorL2 U)

The typed L² field obtained by applying the operator field pointwise.

Equations

• M.apply F = HCPolySupport.toHilbertVectorL2 ⋯

theorem HCPolySupport.PointwiseHilbertVecOperatorField.coeFn_apply {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : ↑↑(M.apply F) =ᵐ[volumeMeasureOn U] M.applyFn F

theorem HCPolySupport.PointwiseHilbertVecOperatorField.apply_add {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F G : ↥(HilbertVectorL2 U)) : M.apply (F + G) = M.apply F + M.apply G

theorem HCPolySupport.PointwiseHilbertVecOperatorField.apply_smul {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (c : ℝ) (F : ↥(HilbertVectorL2 U)) : M.apply (c • F) = c • M.apply F

theorem HCPolySupport.PointwiseHilbertVecOperatorField.norm_apply_le {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : ‖M.apply F‖ ≤ M.opNormBound * ‖F‖

noncomputable def HCPolySupport.PointwiseHilbertVecOperatorField.toContinuousLinearMap {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) : ↥(HilbertVectorL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

The bounded operator on L²(U; \R^d) induced by the pointwise operator field.

Equations

• M.toContinuousLinearMap = { toFun := M.apply, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous M.opNormBound ⋯

@[simp]

theorem HCPolySupport.PointwiseHilbertVecOperatorField.toContinuousLinearMap_apply {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : M.toContinuousLinearMap F = M.apply F

theorem HCPolySupport.PointwiseHilbertVecOperatorField.coeFn_toContinuousLinearMap {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertVecOperatorField U) (F : ↥(HilbertVectorL2 U)) : ↑↑(M.toContinuousLinearMap F) =ᵐ[volumeMeasureOn U] M.applyFn F

noncomputable def HCPolySupport.matToHilbertOperatorLinear (d : ℕ) : Mat d →ₗ[ℝ] HilbertVec d →L[ℝ] HilbertVec d

The real linear map sending a matrix to its action on the Euclidean Hilbert vector space.

Equations

• HCPolySupport.matToHilbertOperatorLinear d = { toFun := HCPolySupport.HilbertVec.applyMat, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HCPolySupport.matToHilbertOperator (d : ℕ) : Mat d →L[ℝ] HilbertVec d →L[ℝ] HilbertVec d

The continuous linear map sending a matrix to its action on the Euclidean Hilbert vector space.

Equations

• HCPolySupport.matToHilbertOperator d = { toLinearMap := HCPolySupport.matToHilbertOperatorLinear d, cont := ⋯ }

theorem HCPolySupport.measurable_matToHilbertOperator {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Mat d} (hA : Measurable A) : Measurable fun (x : α) => (matToHilbertOperator d) (A x)

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

The pointwise Hilbert-vector operator field induced by an elliptic coefficient field on U. Outside U we insert the zero matrix to keep the field globally measurable.

Equations

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

noncomputable def HCPolySupport.hilbertCoeffOperator {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) : ↥(HilbertVectorL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

The bounded operator on L²(U; \R^d) induced by an elliptic coefficient field.

Equations

• HCPolySupport.hilbertCoeffOperator hEll = (HCPolySupport.hilbertCoeffOperatorField hEll).toContinuousLinearMap

theorem HCPolySupport.ae_hilbertCoeffOperator_apply {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (F : ↥(HilbertVectorL2 U)) : ↑↑((hilbertCoeffOperator hEll) F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (HilbertVec.applyMat (a x)) (↑↑F x)

theorem HCPolySupport.hilbertCoeffOperator_toHilbertVectorL2OfVecField {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : (hilbertCoeffOperator hEll) (toHilbertVectorL2OfVecField hf) = toHilbertVectorL2OfVecField ⋯

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

The pointwise Hilbert-vector operator field induced by the symmetric part of an elliptic coefficient field. Outside U we insert the zero matrix to keep the field globally measurable.

Equations

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

noncomputable def HCPolySupport.hilbertSymmCoeffOperator {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) : ↥(HilbertVectorL2 U) →L[ℝ] ↥(HilbertVectorL2 U)

The bounded operator on L²(U; \R^d) induced by the symmetric part of an elliptic coefficient field.

Equations

• HCPolySupport.hilbertSymmCoeffOperator hEll = (HCPolySupport.hilbertSymmCoeffOperatorField hEll).toContinuousLinearMap

theorem HCPolySupport.ae_hilbertSymmCoeffOperator_apply {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) (F : ↥(HilbertVectorL2 U)) : ↑↑((hilbertSymmCoeffOperator hEll) F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (HilbertVec.applyMat (symmPart (a x))) (↑↑F x)

theorem HCPolySupport.hilbertSymmCoeffOperator_toHilbertVectorL2OfVecField {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : (hilbertSymmCoeffOperator hEll) (toHilbertVectorL2OfVecField hf) = toHilbertVectorL2OfVecField ⋯