High-contrast homogenization: Entry.Analysis.PositiveGapMaximal

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

Weighted joint maxima for the positive gap

p.two.grid.transport. The finite maximum is retained in the random centered term; only deterministic mean contributions are summed. Real nested suprema require nonnegativity even for a nonempty finite family, because excluded indices contribute sSup ∅ = 0.

theorem HCPolySupport.HighContrast.Analysis.iSup_mem_finset_eq_finset_sup {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (g : ι → ℝ) (hg : ∀ i ∈ I, 0 ≤ g i) : ⨆ i ∈ ↑I, g i = I.sup' hI g

A nonnegative finite family has the intended real nested supremum. The hypothesis ∀ i ∈ I, 0 ≤ g i cannot be dropped. That unrestricted statement is false: take a proper singleton subset of Bool and g identically -1; the excluded index contributes the empty real supremum 0, while the finite supremum is -1. This added premise is a correct strengthening: every consumer here supplies nonnegative (Schatten/operator-norm) families.

theorem HCPolySupport.HighContrast.Analysis.weightedMax_memLp {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (I : Finset ι) (hI : I.Nonempty) (f : ι → α → ℝ) (hf0 : ∀ i ∈ I, ∀ᵐ (a : α) ∂μ, 0 ≤ f i a) (hf : ∀ i ∈ I, MeasureTheory.MemLp (f i) p μ) : MeasureTheory.MemLp (fun (a : α) => ⨆ i ∈ ↑I, f i a) p μ

The maximum has a genuine finite moment; no totalized-integral shortcut is used.

theorem HCPolySupport.HighContrast.Analysis.weightedMax_nonneg {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (I : Finset ι) (hI : I.Nonempty) (f : ι → α → ℝ) (hf0 : ∀ i ∈ I, ∀ᵐ (a : α) ∂μ, 0 ≤ f i a) : ∀ᵐ (a : α) ∂μ, 0 ≤ ⨆ i ∈ ↑I, f i a

A nonempty joint maximum of nonnegative terms is nonnegative.

theorem HCPolySupport.HighContrast.Analysis.weightedMax_root_memLp {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {N : ℝ} (hN : 0 < N) {t : α → ℝ} (ht : 0 ≤ᵐ[μ] t) (hint : MeasureTheory.Integrable t μ) : MeasureTheory.MemLp (fun (a : α) => t a ^ N⁻¹) (ENNReal.ofReal N) μ ∧ (MeasureTheory.eLpNorm (fun (a : α) => t a ^ N⁻¹) (ENNReal.ofReal N) μ).toReal = (∫ (a : α), t a ∂μ) ^ N⁻¹

An integrable nonnegative envelope has the expected root moment.

theorem HCPolySupport.HighContrast.Analysis.meanPenalty_mono_and_dominates (Q : ℕ) (hQ : 1 ≤ Q) {d : ℕ} {Pm G : BlockMat d} (hPm : IsSymmetricBlockMat Pm) (hG : IsSymmetricBlockMat G) (hI : BlockMatLoewnerLE (Book.Ch02.blockIdentity d) Pm) (hPG : BlockMatLoewnerLE Pm G) : meanPenalty Q Pm ≤ meanPenalty Q G ∧ blockOpNorm G ^ (↑Q - 1) * blockTrace (blockSub G (Book.Ch02.blockIdentity d)) ≤ meanPenalty Q G

The printed mean-penalty conversion uses a positive natural moment. The hypothesis 1 ≤ Q cannot be dropped: without it the domination is false. At Q = 0, with d = 2 and G = 2•I, the right side is 0 while the left side is 2. This added premise is a correct strengthening; the real transport exponent satisfies bigQ ≥ 2, so the actual consumer supplies 1 ≤ Q.

theorem HCPolySupport.HighContrast.Analysis.positiveGap_weighted_joint_absorbed {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 1 < N) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (F G : ι → CoeffSpace d → BlockMat d) (hF : ∀ i ∈ I, SchattenMemLp P N (F i)) (hG : ∀ i ∈ I, SchattenMemLp P N (G i)) (hFpos : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F i a)) (hFG : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F i a) (G i a)) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G i a) α β ∂P); (∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm N (blockSub (G i a) (F i a))) ^ N ∂P) ^ N⁻¹ ≤ (2 * ↑d) ^ N⁻¹ * (∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm N (blockSub (G i a) (MG i))) ^ N ∂P) ^ N⁻¹ + N / (N - 1) * (∑ i ∈ I, w i ^ N * blockOpNorm (MG i) ^ (N - 1) * blockTrace (blockSub (MG i) (MF i))) ^ N⁻¹

Young absorption of the joint maximum; deterministic mean terms alone carry a sum.

theorem HCPolySupport.HighContrast.Analysis.positiveGap_weighted_joint_max (d : ℕ) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 2 ≤ N) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (F G : ι → CoeffSpace d → BlockMat d) (hF : ∀ i ∈ I, SchattenMemLp P N (F i)) (hG : ∀ i ∈ I, SchattenMemLp P N (G i)) (hFpos : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F i a)) (hFG : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F i a) (G i a)) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G i a) α β ∂P); (∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm N (blockSub (F i a) (MF i))) ^ N ∂P) ^ N⁻¹ ≤ (1 + (2 * ↑d) ^ N⁻¹) * (∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm N (blockSub (G i a) (MG i))) ^ N ∂P) ^ N⁻¹ + 2 * (1 + ↑d ^ (1 - N⁻¹)) * (∑ i ∈ I, w i ^ N * blockOpNorm (MG i) ^ (N - 1) * blockTrace (blockSub (MG i) (MF i))) ^ N⁻¹

p.two.grid.transport: the full weighted joint-maximum positive gap.

theorem HCPolySupport.HighContrast.Analysis.positiveGap_weighted_joint_max_pow (d : ℕ) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 2 ≤ N) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (F G : ι → CoeffSpace d → BlockMat d) (hF : ∀ i ∈ I, SchattenMemLp P N (F i)) (hG : ∀ i ∈ I, SchattenMemLp P N (G i)) (hFpos : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F i a)) (hFG : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F i a) (G i a)) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G i a) α β ∂P); ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * blockOpNorm (blockSub (F i a) (MF i))) ^ N ∂P ≤ 2 ^ (N - 1) * (1 + (2 * ↑d) ^ N⁻¹) ^ N * ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm N (blockSub (G i a) (MG i))) ^ N ∂P + 2 ^ (2 * N - 1) * (1 + ↑d ^ (1 - N⁻¹)) ^ N * ∑ i ∈ I, w i ^ N * blockOpNorm (MG i) ^ (N - 1) * blockTrace (blockSub (MG i) (MF i))

p.two.grid.transport: the weighted extension of the fixed-target power estimate at with the operator norm on the left.

theorem HCPolySupport.HighContrast.Analysis.transport_target_max_moment {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} {N : ℝ} (hN : 0 < N) (Z : Finset ι) (hZ : Z.Nonempty) (f : ι → α → ℝ) (hf0 : ∀ z ∈ Z, ∀ᵐ (a : α) ∂P, 0 ≤ f z a) (hf : ∀ z ∈ Z, MeasureTheory.MemLp (f z) (ENNReal.ofReal N) P) : MeasureTheory.Integrable (fun (a : α) => (⨆ z ∈ ↑Z, f z a) ^ N) P ∧ ∫ (a : α), (⨆ z ∈ ↑Z, f z a) ^ N ∂P ≤ ∑ z ∈ Z, ∫ (a : α), f z a ^ N ∂P

A finite target maximum pays the target count after taking moments. The proof records integrability of the actual maximum and every moment.

theorem HCPolySupport.HighContrast.Analysis.transport_joint_envelope_moment {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} {N B : ℝ} (hN : 0 < N) (hB : 0 ≤ B) (Z : Finset ι) (hZ : Z.Nonempty) (f : ι → α → ℝ) (hf0 : ∀ z ∈ Z, ∀ᵐ (a : α) ∂P, 0 ≤ f z a) (hf : ∀ z ∈ Z, MeasureTheory.MemLp (f z) (ENNReal.ofReal N) P) (X : α → ℝ) (hX0 : ∀ᵐ (a : α) ∂P, 0 ≤ X a) (hX : MeasureTheory.MemLp X (ENNReal.ofReal N) P) (hbound : ∀ z ∈ Z, ∀ᵐ (a : α) ∂P, f z a ≤ B * X a) : MeasureTheory.Integrable (fun (a : α) => (⨆ z ∈ ↑Z, f z a) ^ N) P ∧ ∫ (a : α), (⨆ z ∈ ↑Z, f z a) ^ N ∂P ≤ B ^ N * ∫ (a : α), X a ^ N ∂P

A common L^N envelope stays under the joint maximum without an index-count loss. Both sides are genuine integrable moments.