High-contrast homogenization: Entry.Analysis.PositiveGapSupport

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

Positive Gap EccentricityScaleDecay

The scalar, pointwise and mixed-norm estimates the positive-gap theorem l.fixed.geometry.positive.gap is assembled from: the mean-penalty bounds, the pointwise gap inequality, the scalar moment inequalities and the norm comparison. The mixed-norm subtraction estimate also underlies the matrix-averaging lemma l.fixed.geometry.matrix.averaging.

Elementary bounds for the mean penalty

This section proves the deterministic O7 sign consequence from the printed hypothesis I ≤ M: the natural-power mean penalty is nonnegative on every symmetric block above the block identity. The stochastic specialization to normalized adapted means is supplied by the mean-order consequences once the source integrability and order hypotheses are available.

theorem HCPolySupport.HighContrast.Analysis.blockTrace_identity_sub_nonneg {d : ℕ} (M : BlockMat d) (hM : IsSymmetricBlockMat M) (hIM : BlockMatLoewnerLE (Book.Ch02.blockIdentity d) M) : 0 ≤ blockTrace (blockSub M (Book.Ch02.blockIdentity d))

If a symmetric block lies above the block identity, then its printed trace excess is nonnegative.

theorem HCPolySupport.HighContrast.Analysis.meanPenalty_nonneg {d : ℕ} (Q : ℕ) (M : BlockMat d) (hM : IsSymmetricBlockMat M) (hIM : BlockMatLoewnerLE (Book.Ch02.blockIdentity d) M) : 0 ≤ meanPenalty Q M

O7's deterministic sign: the natural-power mean penalty is nonnegative on symmetric blocks above the identity.

Pointwise matrix inequalities for the PositiveGap support layer

This file keeps the deterministic block-matrix part separate from the later random-field assembly. The fixed block operations are used throughout.

theorem HCPolySupport.HighContrast.Analysis.ordered_gap_posSemidef {d : ℕ} {F G : BlockMat d} (hF : IsSymmetricBlockMat F) (hG : IsSymmetricBlockMat G) (hFpos : BlockMatLoewnerLE (ofFullBlockMat 0) F) (hFG : BlockMatLoewnerLE F G) : Matrix.PosSemidef (toFullBlockMat (blockSub G F)) ∧ Matrix.PosSemidef (toFullBlockMat G) ∧ BlockMatLoewnerLE (blockSub G F) G

theorem HCPolySupport.HighContrast.Analysis.blockOpNorm_mono_of_posSemidef {d : ℕ} {D G : BlockMat d} (hD : Matrix.PosSemidef (toFullBlockMat D)) (hG : Matrix.IsHermitian (toFullBlockMat G)) (hDG : BlockMatLoewnerLE D G) : blockOpNorm D ≤ blockOpNorm G

Monotonicity of the real L2 operator norm on positive semidefinite blocks.

theorem HCPolySupport.HighContrast.Analysis.absSchattenNorm_gap_le_opNorm_rpow_mul_trace_rpow {d : ℕ} {D G : BlockMat d} (hD : Matrix.PosSemidef (toFullBlockMat D)) (hG : Matrix.IsHermitian (toFullBlockMat G)) (hDG : BlockMatLoewnerLE D G) {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N D ≤ blockOpNorm G ^ (1 - N⁻¹) * blockTrace D ^ N⁻¹

The first display of the positive-gap proof, valid already for real N ≥ 1.

theorem HCPolySupport.HighContrast.Analysis.trace_le_dim_rpow_mul_absSchattenNorm {d : ℕ} {D : BlockMat d} (hD : Matrix.PosSemidef (toFullBlockMat D)) {N : ℝ} (hN : 1 ≤ N) : blockTrace D ≤ (2 * ↑d) ^ (1 - N⁻¹) * absSchattenNorm N D

Sharp trace/Schatten comparison with the printed 2d factor, including d = 0.

theorem HCPolySupport.HighContrast.Analysis.ordered_trace_le_dim_rpow_mul_opNorm_rpow_mul_trace_rpow {d : ℕ} {D G : BlockMat d} (hD : Matrix.PosSemidef (toFullBlockMat D)) (hG : Matrix.IsHermitian (toFullBlockMat G)) (hDG : BlockMatLoewnerLE D G) {N : ℝ} (hN : 1 ≤ N) : blockTrace D ≤ (2 * ↑d) ^ (1 - N⁻¹) * blockOpNorm G ^ (1 - N⁻¹) * blockTrace D ^ N⁻¹

The trace interpolation used for the deterministic mean gap in the centering step.

Scalar moment inequalities for the PositiveGap support layer

This file records scalar MemLp consequences that do not depend on the operator-valued Schatten infrastructure.

theorem HCPolySupport.HighContrast.Analysis.scalar_holder_power_integrable_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : ℝ} (hN : 1 < N) {f g : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf : MeasureTheory.MemLp f (ENNReal.ofReal N) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal N) μ) : MeasureTheory.Integrable (fun (x : α) => f x ^ (N - 1) * g x) μ ∧ ∫ (x : α), f x ^ (N - 1) * g x ∂μ ≤ (∫ (x : α), (f x ^ (N - 1)) ^ (N / (N - 1)) ∂μ) ^ (1 / (N / (N - 1))) * (∫ (x : α), g x ^ N ∂μ) ^ (1 / N)

theorem HCPolySupport.HighContrast.Analysis.scalar_minkowski_toReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : ℝ} (hN : 1 ≤ N) {f g : α → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal N) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal N) μ) : MeasureTheory.MemLp (fun (x : α) => f x + g x) (ENNReal.ofReal N) μ ∧ (MeasureTheory.eLpNorm (fun (x : α) => f x + g x) (ENNReal.ofReal N) μ).toReal ≤ (MeasureTheory.eLpNorm f (ENNReal.ofReal N) μ).toReal + (MeasureTheory.eLpNorm g (ENNReal.ofReal N) μ).toReal

theorem HCPolySupport.HighContrast.Analysis.scalar_eLpNorm_toReal_eq_root {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : ℝ} (hN : 0 < N) {f : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hf : MeasureTheory.MemLp f (ENNReal.ofReal N) μ) : (MeasureTheory.eLpNorm f (ENNReal.ofReal N) μ).toReal = (∫ (x : α), f x ^ N ∂μ) ^ N⁻¹

Identify the real scalar norm with the rooted moment on its natural nonnegative domain.

theorem HCPolySupport.HighContrast.Analysis.scalar_mixedMoment_root_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : ℝ} (hN : 1 < N) {f g : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf : MeasureTheory.MemLp f (ENNReal.ofReal N) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal N) μ) : (∫ (x : α), f x ^ (N - 1) * g x ∂μ) ^ N⁻¹ ≤ (MeasureTheory.eLpNorm f (ENNReal.ofReal N) μ).toReal ^ (1 - N⁻¹) * (MeasureTheory.eLpNorm g (ENNReal.ofReal N) μ).toReal ^ N⁻¹

The rooted mixed-moment Hölder estimate used in the positive-gap proof.

theorem HCPolySupport.HighContrast.Analysis.scalar_young_mixed {N x y : ℝ} (hN : 1 < N) (hx : 0 ≤ x) (hy : 0 ≤ y) : y ^ (1 - N⁻¹) * x ^ N⁻¹ ≤ (1 - N⁻¹) * y + N⁻¹ * x

Scalar Young inequality in the precise mixed-power form used for absorption.

theorem HCPolySupport.HighContrast.Analysis.scalar_young_absorb {N x y a : ℝ} (hN : 1 < N) (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x ≤ a + y ^ (1 - N⁻¹) * x ^ N⁻¹) : x ≤ y + N / (N - 1) * a

Young absorption with the exact factor N / (N - 1).

theorem HCPolySupport.HighContrast.Analysis.scalar_gap_power_add_le {N a b : ℝ} (hN : 1 ≤ N) (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b) ^ (1 - N⁻¹) ≤ a ^ (1 - N⁻¹) + b ^ (1 - N⁻¹)

Subadditivity of the exponent in the printed positive-gap interpolation.

theorem HCPolySupport.HighContrast.Analysis.scalar_gap_young_absorb {N m x y a : ℝ} (hN : 1 < N) (hm : 0 ≤ m) (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x ≤ a + m ^ ((N - 1) / N ^ 2) * y ^ (1 - N⁻¹) * x ^ N⁻¹) : x ≤ m ^ N⁻¹ * y + N / (N - 1) * a

The paper's exact dimension coefficient after Young absorption; m is 2d.

theorem HCPolySupport.HighContrast.Analysis.scalar_gap_absorption_factor_le_two {N : ℝ} (hN : 2 ≤ N) : N / (N - 1) ≤ 2

The rational factor in the last line of the printed proof.

theorem HCPolySupport.HighContrast.Analysis.scalar_gap_dimension_factor_le {N m : ℝ} (hN : 1 ≤ N) (hm : 0 ≤ m) : (2 * m) ^ (1 - N⁻¹) ≤ 2 * m ^ (1 - N⁻¹)

The dimension simplification in the last line of the printed proof.

Real mixed Schatten norm bridges for the PositiveGap assembly

This file contains only the random-norm consequences needed for the PositiveGap result: the coefficient-one subtraction estimate and the exact constant-field readback on a probability law.

theorem HCPolySupport.HighContrast.Analysis.lqSchattenNorm_sub_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {F G : CoeffSpace d → BlockMat d} (hF : SchattenMemLp P N F) (hG : SchattenMemLp P N G) : (lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (F a) (G a)) ≤ lqSchattenNorm P N F + lqSchattenNorm P N G

Sharp random-field subtraction for the real Schatten mixed norm.

theorem HCPolySupport.HighContrast.Analysis.lqSchattenNorm_const {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 1 ≤ N) (B : BlockMat d) (hB : IsSymmetricBlockMat B) : (lqSchattenNorm P N fun (x : CoeffSpace d) => B) = absSchattenNorm N B

On a probability law, the mixed norm of a deterministic symmetric block is its deterministic Schatten norm.