High-contrast homogenization: Analytic.WeightedBlockCoordOperator

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Weighted coordinate pairings of block L² fields

A localized quadratic observable of a doubled field is an integral of a bounded weight against a product of two of its doubled coordinates. This file realizes such a pairing as the ambient inner product against the image of a bounded multiplication operator, so that it is continuous in both field arguments, and records the resulting measurability rule: the pairing of two strongly measurable sample-dependent fields is a measurable function of the sample.

The operator is the pointwise rank-one field x ↦ eta x • (u ↦ u_alpha • e_beta), which is measurable and uniformly bounded whenever the weight is.

The coordinate units of the doubled Hilbert carrier

def HCPolySupport.HighContrast.Selection.blockCoordUnit {d : ℕ} (alpha : BlockCoord d) : HilbertBlockVec d

The unit of the doubled Hilbert carrier at one doubled coordinate.

Equations

• HCPolySupport.HighContrast.Selection.blockCoordUnit alpha = HCPolySupport.HilbertBlockVec.ofBlockVec (HCPolySupport.blockBasis alpha)

theorem HCPolySupport.HighContrast.Selection.inner_blockCoordUnit {d : ℕ} (alpha : BlockCoord d) (u : HilbertBlockVec d) : inner ℝ (blockCoordUnit alpha) u = toFullBlockVec u.toBlockVec alpha

noncomputable def HCPolySupport.HighContrast.Selection.coordOperator {d : ℕ} (alpha beta : BlockCoord d) : HilbertBlockVec d →L[ℝ] HilbertBlockVec d

The pointwise rank-one operator pairing one doubled coordinate against another.

Equations

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

theorem HCPolySupport.HighContrast.Selection.inner_coordOperator {d : ℕ} (alpha beta : BlockCoord d) (u v : HilbertBlockVec d) : inner ℝ ((coordOperator alpha beta) u) v = toFullBlockVec u.toBlockVec alpha * toFullBlockVec v.toBlockVec beta

The weighted coordinate operator

noncomputable def HCPolySupport.HighContrast.Selection.weightedCoordOperatorField {d : ℕ} {U : Set (Vec d)} {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) (alpha beta : BlockCoord d) : PointwiseHilbertBlockOperatorField U

The pointwise operator field of a weighted coordinate pairing.

Equations

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

noncomputable def HCPolySupport.HighContrast.Selection.weightedCoordOperator {d : ℕ} {U : Set (Vec d)} {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) (alpha beta : BlockCoord d) : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)

The weighted coordinate pairing operator on block L² fields.

Equations

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

theorem HCPolySupport.HighContrast.Selection.inner_pointwiseOperator_eq_integral {d : ℕ} {U : Set (Vec d)} (M : PointwiseHilbertBlockOperatorField U) (F G : ↥(HilbertBlockL2 U)) : inner ℝ (M.toContinuousLinearMap F) G = ∫ (x : Vec d) in U, inner ℝ ((M.field x) (↑↑F x)) (↑↑G x)

The ambient inner product against the image of a pointwise operator field is the integral of the pointwise inner products.

theorem HCPolySupport.HighContrast.Selection.inner_weightedCoordOperator {d : ℕ} {U : Set (Vec d)} {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) (alpha beta : BlockCoord d) (F G : ↥(HilbertBlockL2 U)) : inner ℝ ((weightedCoordOperator hmeas hC hbound alpha beta) F) G = ∫ (x : Vec d) in U, eta x * toFullBlockVec (↑↑F x).toBlockVec alpha * toFullBlockVec (↑↑G x).toBlockVec beta

The weighted coordinate pairing is an ambient inner product.

Measurability of the pairing of two sample-dependent fields