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

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

This file packages the concrete doubled L²(U; \R^{2d}) operator expected by the coarse-graining notes.

The key point is fidelity to the text: the Hilbert-space bilinear form used by the minimization engine should coincide with the averaged pairing

\fint_U X \cdot \mathbf A(a,x) Y.

Since the L² inner product uses the raw integral, the operator recorded here already includes the normalization factor |U|^{-1}.

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

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

This is the analytic input needed to turn a pointwise doubled operator field into an actual bounded operator on L²(U; \R^{2d}).

• field : Vec d → HilbertBlockVec d →L[ℝ] HilbertBlockVec 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.PointwiseHilbertBlockOperatorField.applyFn {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertBlockOperatorField U) (F : ↥(HilbertBlockL2 U)) : Vec d → HilbertBlockVec d

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

Equations

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

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

theorem HCPolySupport.PointwiseHilbertBlockOperatorField.memHilbertBlockL2_applyFn {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertBlockOperatorField U) (F : ↥(HilbertBlockL2 U)) : MemHilbertBlockL2 U (M.applyFn F)

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

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

Equations

• M.apply F = HCPolySupport.toHilbertBlockL2 ⋯

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

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

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

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

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

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

Equations

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

@[simp]

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

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

The operator-valued measurability step for the doubled coefficient field is handled through the full 2d × 2d matrix entries. Since BlockMat d does not carry a measurable/topological structure, we pass through the raw function type BlockCoord d → BlockCoord d → ℝ, which does.

noncomputable def HCPolySupport.fullEntriesToHilbertOperatorLinear (d : ℕ) : (BlockCoord d → BlockCoord d → ℝ) →ₗ[ℝ] HilbertBlockVec d →L[ℝ] HilbertBlockVec d

The real linear map taking full 2d × 2d entries to the corresponding operator on Hilbert block vectors.

Equations

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

noncomputable def HCPolySupport.fullEntriesToHilbertOperator (d : ℕ) : (BlockCoord d → BlockCoord d → ℝ) →L[ℝ] HilbertBlockVec d →L[ℝ] HilbertBlockVec d

The continuous linear map taking full 2d × 2d entries to the corresponding operator on Hilbert block vectors.

Equations

• HCPolySupport.fullEntriesToHilbertOperator d = { toLinearMap := HCPolySupport.fullEntriesToHilbertOperatorLinear d, cont := ⋯ }

theorem HCPolySupport.measurable_fullEntriesToHilbertOperator {d : ℕ} {α : Type u_1} [MeasurableSpace α] {b : α → BlockCoord d → BlockCoord d → ℝ} (hb : Measurable b) : Measurable fun (x : α) => (fullEntriesToHilbertOperator d) (b x)

@[simp]

theorem HCPolySupport.fullEntriesToHilbertOperator_toFullBlockMat {d : ℕ} (B : BlockMat d) : (fullEntriesToHilbertOperator d) (toFullBlockMat B) = HilbertBlockVec.applyBlockMat B

@[simp]

theorem HCPolySupport.symmPart_zero {d : ℕ} : symmPart 0 = 0

@[simp]

theorem HCPolySupport.skewPart_zero {d : ℕ} : skewPart 0 = 0

theorem HCPolySupport.measurable_matrix_transpose_entry {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Fin d → Fin d → ℝ} (hA : Measurable A) (i j : Fin d) : Measurable fun (x : α) => matTranspose (A x) i j

theorem HCPolySupport.measurable_symmPart_entry {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Fin d → Fin d → ℝ} (hA : Measurable A) (i j : Fin d) : Measurable fun (x : α) => symmPart (A x) i j

theorem HCPolySupport.measurable_skewPart_entry {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Fin d → Fin d → ℝ} (hA : Measurable A) (i j : Fin d) : Measurable fun (x : α) => skewPart (A x) i j

theorem HCPolySupport.measurable_matrix_mul_entry {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A B : α → Fin d → Fin d → ℝ} (hA : Measurable A) (hB : Measurable B) (i j : Fin d) : Measurable fun (x : α) => ∑ k : Fin d, A x i k * B x k j

theorem HCPolySupport.measurable_toFullBlockMat_blockCoeffField {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Fin d → Fin d → ℝ} (hA : Measurable A) : Measurable fun (x : α) (α β : BlockCoord d) => toFullBlockMat (blockMatrixOfCoeff (A x)) α β

theorem HCPolySupport.blockMatrixOfCoeffNormSqBound_nonneg (lam Lam : ℝ) : 0 ≤ blockMatrixOfCoeffNormSqBound lam Lam

noncomputable def HCPolySupport.normalizedBlockCoeffOperator {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (x : Vec d) : HilbertBlockVec d →L[ℝ] HilbertBlockVec d

The normalized doubled coefficient operator at a single point x.

The operator is built from the coefficient field restricted to U and extended by zero off U. This matches the note-faithful situation that all analytic statements are made on U, while keeping a genuinely global measurable field for the ambient L²(volume.restrict U) construction.

Equations

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

@[simp]

theorem HCPolySupport.normalizedBlockCoeffOperator_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (x : Vec d) (X : HilbertBlockVec d) : (normalizedBlockCoeffOperator U a x) X = (MeasureTheory.volume U).toReal⁻¹ • (HilbertBlockVec.applyBlockMat (blockCoeffField (restrictCoeffField U a) x)) X

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