Integral

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Quadratic stability, item B′3 (integral form)

The integral half of Lemma 4.1 (l.quadratic.stability) of the high-moment paper (Armstrong–Kuusi–Loher, to appear): stability of the two quadratic minima under an L∞-comparable perturbation of the coefficient field supported on S.

We assume only the two scalar Euler identities at the single test field Y := Zt − Z (no subspace, no minimization, no existence), and derive the sharpened bound with constant 6K.

Chosen integrability package for (h4)

We assume IntegrableOn over U of the five real-valued pairing integrands that actually appear in the proof:

• x ↦ Z·BZ, x ↦ Z·BtZ, x ↦ Y·BtY (three diagonal energies), and
• x ↦ Z·BtY, x ↦ Z·BY (the two cross pairings with the test field Y).

This is the minimal explicit list sufficient for every integral split, the Cauchy–Schwarz step, and the localization; each hypothesis is a concrete ℝ-valued IntegrableOn, directly dischargeable by a consumer holding L² minimizers. (The energy Zt·BtZt needs no separate hypothesis: it equals Z·BtZ + 2 Z·BtY + Y·BtY a.e. by symmetry.)

No EuclideanSpace.

Two elementary analytic helpers

theorem HCPolySupport.integral_sqrt_mul_sqrt_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hf0 : 0 ≤ᵐ[μ] f) (hg0 : 0 ≤ᵐ[μ] g) : ∫ (x : α), √(f x) * √(g x) ∂μ ≤ √(∫ (x : α), f x ∂μ) * √(∫ (x : α), g x ∂μ)

Integral Cauchy–Schwarz for two nonnegative integrable functions: ∫ √f·√g ≤ √(∫f)·√(∫g).

theorem HCPolySupport.sqrt_mul_sqrt_le_half_add {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : √a * √b ≤ (a + b) / 2

AM–GM in the form √a·√b ≤ (a+b)/2 for nonnegative reals.

theorem HCPolySupport.le_sq_of_le_mul_sqrt {G C : ℝ} (hG : 0 ≤ G) (hC : 0 ≤ C) (h : G ≤ C * √G) : G ≤ C ^ 2

If 0 ≤ G and G ≤ C·√G with 0 ≤ C, then G ≤ C².

Data and hypotheses for B′3

theorem HCPolySupport.abs_setIntegral_energy_sub_le {d : ℕ} {U S : Set (Vec d)} {B Bt : Vec d → BlockMat d} {Z Zt : Vec d → BlockVec d} {K : ℝ} (hU : MeasurableSet U) (hS : MeasurableSet S) (hSU : S ⊆ U) (hK : 1 ≤ K) (hae : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsSymmetricBlockMat (B x) ∧ IsSymmetricBlockMat (Bt x) ∧ (∀ (W : BlockVec d), 0 ≤ blockVecDot W (blockMatVecMul (B x) W)) ∧ (∀ (W : BlockVec d), 0 ≤ blockVecDot W (blockMatVecMul (Bt x) W)) ∧ BlockMatLoewnerLE (Bt x) (K • B x) ∧ BlockMatLoewnerLE (B x) (K • Bt x)) (hagree : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (U \ S), B x = Bt x) (hIntBZZ : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (Z x) (blockMatVecMul (B x) (Z x))) U MeasureTheory.volume) (hIntBtZZ : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (Z x) (blockMatVecMul (Bt x) (Z x))) U MeasureTheory.volume) (hIntBtYY : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (Zt x - Z x) (blockMatVecMul (Bt x) (Zt x - Z x))) U MeasureTheory.volume) (hIntBtZY : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (Z x) (blockMatVecMul (Bt x) (Zt x - Z x))) U MeasureTheory.volume) (hIntBZY : MeasureTheory.IntegrableOn (fun (x : Vec d) => blockVecDot (Z x) (blockMatVecMul (B x) (Zt x - Z x))) U MeasureTheory.volume) (hEulerB : ∫ (x : Vec d) in U, blockVecDot (Zt x - Z x) (blockMatVecMul (B x) (Z x)) = 0) (hEulerBt : ∫ (x : Vec d) in U, blockVecDot (Zt x - Z x) (blockMatVecMul (Bt x) (Zt x)) = 0) : |(∫ (x : Vec d) in U, blockVecDot (Zt x) (blockMatVecMul (Bt x) (Zt x))) - ∫ (x : Vec d) in U, blockVecDot (Z x) (blockMatVecMul (B x) (Z x))| ≤ 6 * K * ∫ (x : Vec d) in S, blockVecDot (Z x) (blockMatVecMul (B x) (Z x))

B′3. Stability of the two quadratic minima under an L∞-comparable, S-supported perturbation. Constant 6K.