Deterministic estimate bookkeeping for Proposition 3.5

This file supplies deterministic bookkeeping for blueprint nodes R-322, P-3.5a, R-324 and P-3.5b-det. The first section isolates two reductions used by the analytic proofs:

• the non-splitting pairing class in (3.10) is named once;
• the absolute value of each finite renormalization sum is reduced to the sum of absolute values, both at fixed order and after the truncation sum (3.11).

These are genuine consequences of the frozen definitions, with no analytic bound inserted as a hypothesis.

def Anderson4D.nonSplitPairings (q : ℕ) : Finset (PartialPairing (Fin (2 * q)))

The finite class over which the order-2q renormalization constant is summed in (3.10).

Equations

• Anderson4D.nonSplitPairings q = Finset.filter Anderson4D.IsNonSplit Finset.univ

@[simp]

theorem Anderson4D.mem_nonSplitPairings {q : ℕ} {σ : PartialPairing (Fin (2 * q))} : σ ∈ nonSplitPairings q ↔ IsNonSplit σ

noncomputable def Anderson4D.detJAbsIntegrand (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xtJ : Fin (2 * q) → T4) : ℝ

The nonnegative absolute-value form of the closed J integrand. Only the extracted difference factors can change sign: free Green factors and covariance factors are nonnegative.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.detJAbsIntegrand_nonneg (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xtJ : Fin (2 * q) → T4) : 0 ≤ detJAbsIntegrand ρ ε q σ xtJ

theorem Anderson4D.abs_detJintegrand_eq_detJAbsIntegrand (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xtJ : Fin (2 * q) → T4) : |detJintegrand ρ ε q σ xtJ| = detJAbsIntegrand ρ ε q σ xtJ

Absolute value distributes through the closed formula exactly.

noncomputable def Anderson4D.renormC2qTerm (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) : ℝ

One summand of the order-2q renormalization constant.

Equations

• Anderson4D.renormC2qTerm ρ lam ε q σ = ∫ (z : Anderson4D.T4), Anderson4D.detJ ρ lam ε q σ z 0 ∂Anderson4D.paperMeasure

theorem Anderson4D.abs_renormC2qTerm_le_integral_abs (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) : |renormC2qTerm ρ lam ε q σ| ≤ ∫ (z : T4), |detJ ρ lam ε q σ z 0| ∂paperMeasure

Move the absolute value through the final spatial integral in one renormalization summand.

theorem Anderson4D.abs_detJ_succ_le_integral_abs (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (z w : T4) : |detJ ρ lam ε (q + 1) σ z w| ≤ |lamEps lam ε| ^ (2 * (q + 1)) * ∫ (v : Fin (2 * q) → T4), |detJintegrand ρ ε (q + 1) σ fun (j : Fin (2 * (q + 1))) => assemble z w v (Fin.cast ⋯ j)| ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure

Move absolute values through the internal J integral at positive order. The even coupling power is retained exactly; no coarse constant is introduced at this bookkeeping stage.

theorem Anderson4D.abs_detJ_succ_le_integral_detJAbs (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (z w : T4) : |detJ ρ lam ε (q + 1) σ z w| ≤ |lamEps lam ε| ^ (2 * (q + 1)) * ∫ (v : Fin (2 * q) → T4), detJAbsIntegrand ρ ε (q + 1) σ fun (j : Fin (2 * (q + 1))) => assemble z w v (Fin.cast ⋯ j) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure

Positive-integrand version of abs_detJ_succ_le_integral_abs, ready for the primitive-interval reduction.

theorem Anderson4D.renormC2q_eq_sum (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : renormC2q ρ lam ε q = ∑ σ ∈ nonSplitPairings q, renormC2qTerm ρ lam ε q σ

The named pairing class and summand recover the frozen definition of renormC2q definitionally.

theorem Anderson4D.abs_renormC2q_le_sum_abs (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : |renormC2q ρ lam ε q| ≤ ∑ σ ∈ nonSplitPairings q, |renormC2qTerm ρ lam ε q σ|

Triangle-inequality reduction for (3.22) at one perturbative order.

theorem Anderson4D.abs_renormC2q_le_sum_integral_abs (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : |renormC2q ρ lam ε q| ≤ ∑ σ ∈ nonSplitPairings q, ∫ (z : T4), |detJ ρ lam ε q σ z 0| ∂paperMeasure

Integral majorant for the complete order-2q constant. This is the entry point of the interval-reduction argument in paper §4.1.

theorem Anderson4D.abs_renormCEps_le_sum_abs (ρ : SmoothCutoff) (lam ε : ℝ) : |renormCEps ρ lam ε| ≤ ∑ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q|

Triangle-inequality reduction after summing the explicit constants over 1 ≤ q ≤ A. This is the deterministic ledger used in the parametrix remainder estimate (3.21).

theorem Anderson4D.abs_renormCEps_le_sum_pairing_abs (ρ : SmoothCutoff) (lam ε : ℝ) : |renormCEps ρ lam ε| ≤ ∑ q ∈ Finset.Icc 1 (truncOrder ε), ∑ σ ∈ nonSplitPairings q, |renormC2qTerm ρ lam ε q σ|

Combining the two finite triangle inequalities reduces the whole renormalization constant to absolute values of individual J terms.