High-contrast homogenization: Provider.Response.AnnealedWeakQuantity

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

The annealed weak quantities as integrals of samplewise majorants

The weak quantities of the profile are squared L² norms of samplewise weak seminorms. A samplewise estimate for a term of the response split therefore has to be turned into an estimate for the expectation of that term, and its samplewise majorant has to be recognized as the integrand whose integral is the weak quantity.

Both steps are recorded here. The squared L² norm of an extended-nonnegative observable is the integral of its square, which identifies the weak quantities with integrals of the squared weak roots; and the expectation of a real observable is dominated by the integral of its samplewise majorant, which is the Jensen step. Nothing about the geometry of the weak seminorm is used.

The squared norm as an integral

theorem HCPolySupport.HighContrast.Response.eLpNorm_two_sq_eq_lintegral_sq {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (g : α → ENNReal) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.eLpNorm g 2 μ ^ 2 = ∫⁻ (a : α), g a ^ 2 ∂μ

The square of the L² norm of an extended-nonnegative observable is the integral of its square.

theorem HCPolySupport.HighContrast.Response.profilePrimalWeakQuantity_eq_lintegral {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hroot : MeasureTheory.AEStronglyMeasurable (profilePrimalWeakRoot m0 hq t sample p r (profilePrimalCenter P hq t sample p r)) P) : profilePrimalWeakQuantity P m0 hq t sample p r = ∫⁻ (a : CoeffSpace d), profilePrimalWeakRoot m0 hq t sample p r (profilePrimalCenter P hq t sample p r) a ^ 2 ∂P

The primal weak quantity is the integral of the squared primal weak root.

theorem HCPolySupport.HighContrast.Response.profileAdjointWeakQuantity_eq_lintegral {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hroot : MeasureTheory.AEStronglyMeasurable (profileAdjointWeakRoot m0 hq t sample p r (profileAdjointCenter P hq t sample p r)) P) : profileAdjointWeakQuantity P m0 hq t sample p r = ∫⁻ (a : CoeffSpace d), profileAdjointWeakRoot m0 hq t sample p r (profileAdjointCenter P hq t sample p r) a ^ 2 ∂P

The coefficient-transpose weak quantity is the integral of the squared adjoint weak root.

The Jensen step

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_le_mul_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {C : ENNReal} {g : α → ENNReal} (hC : C ≠ ⊤) (hmajorant : ∀ᵐ (a : α) ∂μ, ENNReal.ofReal |f a| ≤ C * g a) : ENNReal.ofReal |∫ (a : α), f a ∂μ| ≤ C * ∫⁻ (a : α), g a ∂μ

The expectation against a samplewise majorant. A samplewise bound by a constant multiple of an extended-nonnegative majorant bounds the expectation by the same multiple of the integral of that majorant.

The weak components

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_le_mul_profilePrimalWeakQuantity {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) {term : CoeffSpace d → ℝ} {Cdiv : ℝ} (hmajorant : ∀ᵐ (a : CoeffSpace d) ∂P, ENNReal.ofReal |term a| ≤ ENNReal.ofReal Cdiv * profilePrimalWeakRoot m0 hq t sample p r (profilePrimalCenter P hq t sample p r) a ^ 2) : ENNReal.ofReal |∫ (a : CoeffSpace d), term a ∂P| ≤ ENNReal.ofReal Cdiv * profilePrimalWeakQuantity P m0 hq t sample p r

The primal weak component. A samplewise bound by a multiple of the squared primal weak root becomes a bound for the expectation by the same multiple of the primal weak quantity.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_le_mul_profileAdjointWeakQuantity {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) {term : CoeffSpace d → ℝ} {Cdiv : ℝ} (hmajorant : ∀ᵐ (a : CoeffSpace d) ∂P, ENNReal.ofReal |term a| ≤ ENNReal.ofReal Cdiv * profileAdjointWeakRoot m0 hq t sample p r (profileAdjointCenter P hq t sample p r) a ^ 2) : ENNReal.ofReal |∫ (a : CoeffSpace d), term a ∂P| ≤ ENNReal.ofReal Cdiv * profileAdjointWeakQuantity P m0 hq t sample p r

The coefficient-transpose weak component.

The two-step form