High-contrast homogenization: Entry.Analysis.InverseJensen

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

Inverse Jensen and the annealed primal–adjoint order

Ordinary support for p.global.selection and near e.two.grid.source.normalization, on the CG block and coefficient carriers. The pathwise input is derived from response nonnegativity for both the original and adjoint coefficient fields. The deterministic two-sign reduction uses Mathlib's Schur complement and elementary quadratic identities; it needs no new spectral theorem.

Inverse Jensen integrates a fixed variational test vector and then uses the attained maximum. The inverse entries are separately proved integrable, by domination from the pathwise order and the measurable determinant/adjugate formula. Deterministic swap conjugation commutes with the entrywise integral; inversion is never commuted with it.

The rounded-grid endpoints discharge integrability and positive definiteness under the standing stationary dagger law. The version adaptedMean_swapConj_le_of_integrable also covers the literal Euclidean grid: it takes any invertible grid and the existing HasIntegrableCoarseBlock receipt, and the inverse-conjugate order it supplies gives the determinant lower bound for those grids. This keeps the rounded-grid order independent of the Euclidean-grid identification. No unit-range or extra source-window premise is needed here.

The generic matrix results include empty finite index sets. Actual adapted domains require NeZero d; the standing-law corollaries carry 2 ≤ d. Strict positivity is proved before every use of inverse cancellation and determinant positivity. The reference-block order for E is not asserted by this file.

theorem HCPolySupport.HighContrast.Analysis.two_inner_sub_quadratic_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι ℝ} (hM : M.PosDef) (x y : ι → ℝ) : 2 * x ⬝ᵥ y - y ⬝ᵥ M.mulVec y ≤ x ⬝ᵥ M⁻¹.mulVec x

Every variational test lies below the inverse quadratic form.

theorem HCPolySupport.HighContrast.Analysis.isGreatest_two_inner_sub_quadratic {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι ℝ} (hM : M.PosDef) (x : ι → ℝ) : IsGreatest {t : ℝ | ∃ (y : ι → ℝ), t = 2 * x ⬝ᵥ y - y ⬝ᵥ M.mulVec y} (x ⬝ᵥ M⁻¹.mulVec x)

The inverse quadratic form is the attained maximum of the affine-quadratic tests.

theorem HCPolySupport.HighContrast.Analysis.inner_inv_integral_le_integral_inner_inv {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (A : Ω → Matrix ι ι ℝ) (hAE : ∀ᵐ (a : Ω) ∂P, (A a).PosDef) (hA : ∀ (i j : ι), MeasureTheory.Integrable (fun (a : Ω) => A a i j) P) (hAinv : ∀ (i j : ι), MeasureTheory.Integrable (fun (a : Ω) => (A a)⁻¹ i j) P) (hbar : (Matrix.of fun (i j : ι) => ∫ (a : Ω), A a i j ∂P).PosDef) (x : ι → ℝ) : x ⬝ᵥ (Matrix.of fun (i j : ι) => ∫ (a : Ω), A a i j ∂P)⁻¹.mulVec x ≤ x ⬝ᵥ (Matrix.of fun (i j : ι) => ∫ (a : Ω), (A a)⁻¹ i j ∂P).mulVec x

Inverse Jensen: a fixed variational test vector is integrated before maximizing.

theorem HCPolySupport.HighContrast.Analysis.blockMatLoewnerLE_swapConj_inv_iff {d : ℕ} {F : BlockMat d} (hsymm : IsSymmetricBlockMat F) (hpos : Matrix.PosDef (toFullBlockMat F)) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat F)⁻¹ * toFullBlockMat (blockSwap d))) F ↔ BlockMatLoewnerLE (blockSwap d) F ∧ BlockMatLoewnerLE (blockScale (-1) (blockSwap d)) F

The two signs characterize the inverse-conjugate order, by the Schur complement.

theorem HCPolySupport.HighContrast.Analysis.blockMatLoewnerLE_swapConj_coarseBlock {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (a : CoeffSpace d) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat (coarseBlock (adaptedCellTranslate q j y) a))⁻¹ * toFullBlockMat (blockSwap d))) (coarseBlock (adaptedCellTranslate q j y) a)

Pathwise primal–adjoint order on the actual qualitative coefficient carrier.

theorem HCPolySupport.HighContrast.Analysis.integrable_inv_coarseBlock_adapted {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (hint : HasIntegrableCoarseBlock P (adaptedCellTranslate q j y)) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (toFullBlockMat (coarseBlock (adaptedCellTranslate q j y) a))⁻¹ α β) P

The inverse entries are integrable by the pathwise order, not by an inverse/mean exchange.

theorem HCPolySupport.HighContrast.Analysis.adaptedMean_swapConj_le_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (q : Mat d) (hq : IsUnit q) (j : ℤ) (hint : HasIntegrableCoarseBlock P (adaptedCell q j)) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat (adaptedMean P q j))⁻¹ * toFullBlockMat (blockSwap d))) (adaptedMean P q j)

Any invertible grid, including the literal Euclidean grid, with its finite-mean receipt.

theorem HCPolySupport.HighContrast.Analysis.adaptedMean_swapConj_le {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j))⁻¹ * toFullBlockMat (blockSwap d))) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)

The annealed primal–adjoint order under the standing stationary dagger law.

theorem HCPolySupport.HighContrast.Analysis.one_le_det_adaptedMean {d : ℕ} (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : 1 ≤ Matrix.det (toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j))

The full doubled determinant of the actual adapted mean is at least one.