High-contrast homogenization: Entry.Response.Core.GalerkinOptimizerReadout #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Galerkin realization and readout of the response optimizer #
On a general open response cell, this file re-derives the measurable canonical response optimizer
from the library's countable-energy Hilbert-space presentation and the Chapter-4 realization,
constructing the correction space, the quadratic energy functional and its minimizer, and proving
the measurability of the resulting bilinear form, inner product and readout. It then recovers the
canonical optimizer's block state and its coefficient-on-a-slice presentation from the doubled
minimizer, showing the readout is almost everywhere the full block vector, that it agrees under
congruence, and that a potential built from it has zero trace on the book's boundary presentation.
This furnishes the measurable response-optimizer readout that the response-transfer estimate
p.response.transfer consumes.
Galerkin selection on a response cell #
This is the general-open-cell part of the measurable response-maximizer chain. It is re-derived
on the current RegCoeffField carrier from CG's Chapter-4 Hilbert realization and this
library's public countable-energy presentation.
noncomputable def
HCPolySupport.HighContrast.Multiscale.responseCellMuSystem
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
:
The doubled operator system on a general positive-volume response cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.HighContrast.Multiscale.responseCellMuHilbert
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
:
MuHilbertRealization U ↑a
The Hilbert realization of responseCellMuSystem.
Equations
Instances For
def
HCPolySupport.HighContrast.Multiscale.responseSliceOf
{d : ℕ}
{Om : Type u_1}
{U : Set (Vec d)}
{k : ℕ}
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(w : Om)
:
The carrier slice datum at a parameter.
Equations
- HCPolySupport.HighContrast.Multiscale.responseSliceOf hSlice w = ⟨(A w).toFun, ⋯⟩
Instances For
theorem
HCPolySupport.HighContrast.Multiscale.constantField_responseCellMuHilbert
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
:
theorem
HCPolySupport.HighContrast.Multiscale.correctionSpace_responseCellMuHilbert
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
:
theorem
HCPolySupport.HighContrast.Multiscale.responseCellMuCandidate_sub_constant_mem
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(P0 : BlockVec d)
(Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U))
:
Selection.cellMuCandidate P0 Y - (responseCellMuHilbert hvol a).constantField P0 ∈ (responseCellMuHilbert hvol a).correctionSpace.correctionSpace
theorem
HCPolySupport.HighContrast.Multiscale.quadraticEnergy_responseCellMuCandidate
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(P0 : BlockVec d)
(Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U))
:
quadraticEnergy (responseCellMuHilbert hvol a).energyBilin (Selection.cellMuCandidate P0 Y) = blockEnergyAverage U (↑a) (canonicalMuGeneratorAffineField P0 Y)
theorem
HCPolySupport.HighContrast.Multiscale.responseMu_eq_quadraticEnergy_minimizer
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(P0 : BlockVec d)
:
Mu U P0 ↑a = quadraticEnergy (responseCellMuHilbert hvol a).energyBilin ((responseCellMuHilbert hvol a).minimizerMap P0)
On a general response cell, Mu is the energy of the Hilbert minimizer.
theorem
HCPolySupport.HighContrast.Multiscale.tendsto_responseCellMuCandidate_selected
{d : ℕ}
{Om : Type u_1}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hvol : 0 < (MeasureTheory.volume U).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(P0 : BlockVec d)
(ξ : ℕ → ↥(canonicalMuBlockCorrectionGeneratorSubmodule U))
(index : ℕ → Om → ℕ)
(hindex :
∀ (m : ℕ) (w : Om),
blockEnergyAverage U (A w).toFun (canonicalMuGeneratorAffineField P0 (ξ (index m w))) ≤ Mu U P0 (A w).toFun + 1 / (↑m + 1))
(w : Om)
:
Filter.Tendsto (fun (m : ℕ) => Selection.cellMuCandidate P0 (ξ (index m w))) Filter.atTop
(nhds ((responseCellMuHilbert hvol (responseSliceOf hSlice w)).minimizerMap P0))
Near-minimal fixed Galerkin competitors converge pointwise to the response-cell minimizer.
theorem
HCPolySupport.HighContrast.Multiscale.stronglyMeasurable_responseCellMuMinimizer
{d : ℕ}
{Om : Type u_1}
[mOm : MeasurableSpace Om]
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfin : MeasureTheory.volume U ≠ ⊤)
(hvol : 0 < (MeasureTheory.volume U).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(hEntry :
∀ (i j : Fin d) {φ : Vec d → ℝ},
ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (w : Om) => entryTestR i j φ (A w))
(P0 : BlockVec d)
:
MeasureTheory.StronglyMeasurable fun (w : Om) => (responseCellMuHilbert hvol (responseSliceOf hSlice w)).minimizerMap P0
The doubled Mu minimizer on a general positive-volume open cell is strongly measurable in
any regular-field parameter whose supported smooth entry tests are measurable on one quantitative
ellipticity slice.
theorem
HCPolySupport.HighContrast.Multiscale.measurable_inner_responseCellMuMinimizer
{d : ℕ}
{Om : Type u_1}
[mOm : MeasurableSpace Om]
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfin : MeasureTheory.volume U ≠ ⊤)
(hvol : 0 < (MeasureTheory.volume U).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(hEntry :
∀ (i j : Fin d) {φ : Vec d → ℝ},
ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (w : Om) => entryTestR i j φ (A w))
(P0 : BlockVec d)
(y : ↥(HilbertBlockL2 U))
:
Measurable fun (w : Om) => inner ℝ y ((responseCellMuHilbert hvol (responseSliceOf hSlice w)).minimizerMap P0)
Every fixed Hilbert-space coordinate of the general-cell minimizer is measurable.
theorem
HCPolySupport.HighContrast.Multiscale.measurable_readout_responseCellMuMinimizer
{d : ℕ}
{Om : Type u_1}
[mOm : MeasurableSpace Om]
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfin : MeasureTheory.volume U ≠ ⊤)
(hvol : 0 < (MeasureTheory.volume U).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(hEntry :
∀ (i j : Fin d) {φ : Vec d → ℝ},
ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (w : Om) => entryTestR i j φ (A w))
(P0 : BlockVec d)
{R : Om → ↥(HilbertBlockL2 U) → ℝ}
(hRcont : ∀ (w : Om), Continuous (R w))
(hRmeas :
∀ (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)),
Measurable fun (w : Om) => R w (Selection.cellMuCandidate P0 Y))
:
Measurable fun (w : Om) => R w ((responseCellMuHilbert hvol (responseSliceOf hSlice w)).minimizerMap P0)
Continuous sample-dependent readouts transfer from fixed Galerkin competitors to the response-cell minimizer.
theorem
HCPolySupport.HighContrast.Multiscale.energyBilin_responseCellMuCandidate_eq_blockPairingAverage
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U).toReal)
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(P0 : BlockVec d)
{Y : BlockState d}
(hY : MemBlockL2 U Y.eval)
(Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U))
:
((responseCellMuHilbert hvol a).energyBilin (toHilbertBlockL2OfBlockField hY)) (Selection.cellMuCandidate P0 Z) = blockPairingAverage U (↑a) (canonicalMuGeneratorAffineField P0 Z) Y
The energy pairing against a fixed state, evaluated at a Galerkin competitor, is the corresponding block pairing average.
theorem
HCPolySupport.HighContrast.Multiscale.measurable_energyBilin_responseCellMuMinimizer
{d : ℕ}
{Om : Type u_1}
[mOm : MeasurableSpace Om]
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfin : MeasureTheory.volume U ≠ ⊤)
(hvol : 0 < (MeasureTheory.volume U).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun)
(hEntry :
∀ (i j : Fin d) {φ : Vec d → ℝ},
ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (w : Om) => entryTestR i j φ (A w))
(P0 : BlockVec d)
{Y : BlockState d}
(hY : MemBlockL2 U Y.eval)
:
Measurable fun (w : Om) =>
((responseCellMuHilbert hvol (responseSliceOf hSlice w)).energyBilin (toHilbertBlockL2OfBlockField hY))
((responseCellMuHilbert hvol (responseSliceOf hSlice w)).minimizerMap P0)
The coefficient-dependent doubled energy pairing of the minimizer against a fixed block state is measurable.
Recovery of the canonical response optimizer from the doubled minimizer #
noncomputable def
HCPolySupport.HighContrast.Multiscale.canonicalOptimizerBlockState
{d : ℕ}
(U : Book.Ch02.Domain d)
(aU : Book.Ch02.CoeffOn U)
(p q : Vec d)
:
The complete doubled state of the Chapter-2 canonical response maximizer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.HighContrast.Multiscale.canonicalOptimizerStateReadout
{d : ℕ}
(U : Book.Ch02.Domain d)
(aU : Book.Ch02.CoeffOn U)
(p q : Vec d)
(α : BlockCoord d)
(η : Vec d → ℝ)
:
A weighted coordinate readout of the canonical optimizer state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.HighContrast.Multiscale.canonicalOptimizerStateReadout_congr
{d : ℕ}
{U : Book.Ch02.Domain d}
{aU bU : Book.Ch02.CoeffOn U}
(h : aU.AEEq bU)
(p q : Vec d)
(α : BlockCoord d)
(η : Vec d → ℝ)
:
noncomputable def
HCPolySupport.HighContrast.Multiscale.responseCoeffOnOfSlice
{d : ℕ}
(U : Book.Ch02.Domain d)
{k : ℕ}
(A : RegCoeffField d)
(hk : AEEQuantitativeEllipticSlice U.carrier k A.toFun)
:
A regular field on a quantitative slice, packaged as a Chapter-2 coefficient object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.HighContrast.Multiscale.toHilbertBlockL2_eq_responseMinimizer_of_isDoubledMuMinimizer
{d : ℕ}
{U : Book.Ch02.Domain d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U.carrier).toReal)
{aU : Book.Ch02.CoeffOn U}
(hk : AEEQuantitativeEllipticSlice U.carrier k aU.toCoeffField)
(P0 : BlockVec d)
{X : Book.Ch02.DoubledField d}
(hX : Book.Ch02.IsDoubledMuMinimizer U aU P0 X)
(hAdm : IsBlockMuAdmissible U.carrier P0 { potential := X.potential, flux := X.flux })
:
A pointwise Chapter-2 doubled minimizer represents the same Hilbert minimizer selected by the general-cell Galerkin construction.
theorem
HCPolySupport.HighContrast.Multiscale.ae_toFullBlockVec_canonicalOptimizerBlockState
{d : ℕ}
{U : Book.Ch02.Domain d}
{aU : Book.Ch02.CoeffOn U}
(p q : Vec d)
(α : BlockCoord d)
{X : Book.Ch02.DoubledField d}
(hX : Book.Ch02.IsDoubledMuMinimizer U aU (-p, q) X)
:
(fun (x : Vec d) => toFullBlockVec (canonicalOptimizerBlockState U aU p q x) α) =ᵐ[volumeMeasureOn U.carrier]
fun (x : Vec d) =>
toFullBlockVec (X.eval x) α + toFullBlockVec (blockMatVecMul (blockCoeffField aU.toCoeffField x) (X.eval x)) (Sum.swap α)
Coordinatewise a.e. recovery of the canonical optimizer's complete doubled state.
theorem
HCPolySupport.HighContrast.Multiscale.integral_weighted_canonicalOptimizerBlockState
{d : ℕ}
{U : Book.Ch02.Domain d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)]
{k : ℕ}
(hvol : 0 < (MeasureTheory.volume U.carrier).toReal)
{aU : Book.Ch02.CoeffOn U}
(hk : AEEQuantitativeEllipticSlice U.carrier k aU.toCoeffField)
(p q : Vec d)
(α : BlockCoord d)
{η : Vec d → ℝ}
(hη : MemScalarL2 U.carrier η)
:
∫ (x : Vec d) in U.carrier, η x * toFullBlockVec (canonicalOptimizerBlockState U aU p q x) α = inner ℝ (toHilbertBlockL2OfBlockField ⋯) ((responseCellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).minimizerMap (-p, q)) + (MeasureTheory.volume U.carrier).toReal * ((responseCellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).energyBilin (toHilbertBlockL2OfBlockField ⋯))
((responseCellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).minimizerMap (-p, q))
Weighted coordinates of the canonical optimizer are the sum of an inner-product readout and an energy-bilinear readout of the doubled minimizer.
theorem
HCPolySupport.HighContrast.Multiscale.measurable_integral_weighted_canonicalOptimizerBlockState
{d : ℕ}
{Om : Type u_1}
[mOm : MeasurableSpace Om]
{U : Book.Ch02.Domain d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)]
{k : ℕ}
(hUopen : IsOpen U.carrier)
(hUfin : MeasureTheory.volume U.carrier ≠ ⊤)
(hvol : 0 < (MeasureTheory.volume U.carrier).toReal)
{A : Om → RegCoeffField d}
(hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U.carrier k (A w).toFun)
(hEntry :
∀ (i j : Fin d) {φ : Vec d → ℝ},
ContDiff ℝ (↑⊤) φ →
HasCompactSupport φ → tsupport φ ⊆ U.carrier → Measurable fun (w : Om) => entryTestR i j φ (A w))
(aU : Om → Book.Ch02.CoeffOn U)
(haU : ∀ (w : Om), (aU w).toCoeffField = (A w).toFun)
(p q : Vec d)
(α : BlockCoord d)
{η : Vec d → ℝ}
(hη : MemScalarL2 U.carrier η)
:
Measurable fun (w : Om) =>
∫ (x : Vec d) in U.carrier, η x * toFullBlockVec (canonicalOptimizerBlockState U (aU w) p q x) α
Weighted coordinate readouts of the canonical optimizer are measurable on one quantitative ellipticity slice of a general response cell.