High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1WeightedLeastSquaresCore

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

Linear least-squares coordinates in a coercive Hilbert energy

For an injective finite-dimensional trial map, coercive Hilbert minimization selects a unique residual. Pulling its correction back through the trial map gives a linear parameter selector.

noncomputable def HCPolySupport.HighContrast.Root.closedLinearRange {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : E →ₗ[ℝ] H) (hclosed : IsClosed ↑T.range) : ClosedSubmodule ℝ H

A closed-subspace package for a closed linear range.

Equations

• HCPolySupport.HighContrast.Root.closedLinearRange T hclosed = { toSubmodule := T.range, isClosed' := hclosed }

noncomputable def HCPolySupport.HighContrast.Root.weightedLeastSquaresSlopeMap {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →ₗ[ℝ] H) (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑T.range) (B : H →L[ℝ] H →L[ℝ] ℝ) (hB : IsCoercive B) (J : E →L[ℝ] H) : E →ₗ[ℝ] E

The coefficient-weighted least-squares slope selector. The correction of the affine Hilbert minimizer lies in the trial range; injectivity of the trial map identifies that correction with a unique parameter.

Equations

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

theorem HCPolySupport.HighContrast.Root.trialMap_weightedLeastSquaresSlopeMap {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →ₗ[ℝ] H) (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑T.range) (B : H →L[ℝ] H →L[ℝ] ℝ) (hB : IsCoercive B) (J : E →L[ℝ] H) (e : E) : T ((weightedLeastSquaresSlopeMap T hT hclosed B hB J) e) = -↑((correctionMap (closedLinearRange T hclosed) B hB) (J e))

The selected trial field is exactly the correction of the affine Hilbert minimizer.

theorem HCPolySupport.HighContrast.Root.residual_weightedLeastSquaresSlopeMap {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →ₗ[ℝ] H) (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑T.range) (B : H →L[ℝ] H →L[ℝ] ℝ) (hB : IsCoercive B) (J : E →L[ℝ] H) (e : E) : J e - T ((weightedLeastSquaresSlopeMap T hT hclosed B hB J) e) = (affineMinimizerMap (closedLinearRange T hclosed) B hB) (J e)

The residual defined by the slope selector is the affine Hilbert minimizer.

theorem HCPolySupport.HighContrast.Root.quadraticEnergy_residual_weightedLeastSquaresSlopeMap_le {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →ₗ[ℝ] H) (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑T.range) {B : H →L[ℝ] H →L[ℝ] ℝ} (hB : IsCoercive B) (hBsymm : ∀ (x y : H), (B x) y = (B y) x) (J : E →L[ℝ] H) (e b : E) : quadraticEnergy B (J e - T ((weightedLeastSquaresSlopeMap T hT hclosed B hB J) e)) ≤ quadraticEnergy B (J e - T b)

The selected residual minimizes the coercive quadratic energy among all trial slopes.

theorem HCPolySupport.HighContrast.Root.eq_weightedLeastSquaresSlopeMap_of_quadraticEnergy_le {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →ₗ[ℝ] H) (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑T.range) {B : H →L[ℝ] H →L[ℝ] ℝ} (hB : IsCoercive B) (hBsymm : ∀ (x y : H), (B x) y = (B y) x) (J : E →L[ℝ] H) (e b : E) (hle : quadraticEnergy B (J e - T b) ≤ quadraticEnergy B (J e - T ((weightedLeastSquaresSlopeMap T hT hclosed B hB J) e))) : b = (weightedLeastSquaresSlopeMap T hT hclosed B hB J) e

The selected slope is the unique slope whose residual has no larger energy than the canonical least-squares residual.