Reduction of the pure-cross fibres to the permutation multi-window

A pure-cross refined fibre consists of entities ⟨id, id, π⟩: both half chains are plain (m+1 Green edges, no extraction, no within covariance), and the m covariance legs are all cross legs, indexed by a set of bijections π. This file proves, at every order m:

• the identity-pairing half integrand is the plain Green chain;
• the summed fibre is one physical integral of a nonnegative density: the two plain chains times the permutation-summed cross covariance — no triangle inequality across the fibre is used;
• the permanent bound: the permutation-summed cross covariance is pointwise at most the product of its m row sums, absorbing the factorial fibre cardinality into m diagonal-window rows.

The identity pairing has plain chains

theorem Anderson4D.r324LedgerThree_extract_id (m : ℕ) : extract PartialPairing.id = []

Nothing is extracted from the identity pairing: a relative fully paired interval would need its left endpoint moved.

theorem Anderson4D.r324LedgerThree_pairSupport_id (m : ℕ) : PartialPairing.id.pairSupport = ∅

The identity pairing moves nothing.

theorem Anderson4D.r324LedgerThree_detIntegrand_id (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (xt : Fin (m + 2) → T4) : detIntegrand ρ ε m PartialPairing.id xt = ∏ e : Fin (m + 1), greenFn (xt e.castSucc - xt e.succ)

The identity-pairing integrand is the plain Green chain: no edge is excluded, no difference factor and no within covariance appears.

theorem Anderson4D.r324LedgerThree_chain_nonneg (m : ℕ) (xt : Fin (m + 2) → T4) : 0 ≤ ∏ e : Fin (m + 1), greenFn (xt e.castSucc - xt e.succ)

The plain Green chain is nonnegative.

Pure-cross entities are permutation entities

theorem Anderson4D.R324LedgerThreeAllCrossEntity.eq_mk {m : ℕ} {e : MomentContraction m} (h : R324LedgerThreeAllCrossEntity e) : ∃ (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles), e = ⟨PartialPairing.id, ⟨PartialPairing.id, π⟩⟩

A pure-cross entity is literally ⟨id, id, π⟩ for a bijection π of the identity singles.

theorem Anderson4D.r324LedgerThree_mk_injective {m : ℕ} {π π' : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles} (h : ⟨PartialPairing.id, ⟨PartialPairing.id, π⟩⟩ = ⟨PartialPairing.id, ⟨PartialPairing.id, π'⟩⟩) : π = π'

The permutation entities are distinct for distinct bijections.

The permanent bound

theorem Anderson4D.r324LedgerThree_sum_equiv_prod_le_prod_sum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (c : ι → κ → ℝ) (hc : ∀ (i : ι) (j : κ), 0 ≤ c i j) : ∑ π : ι ≃ κ, ∏ i : ι, c i (π i) ≤ ∏ i : ι, ∑ j : κ, c i j

Permanent bound by row sums. A sum over bijections of products of nonnegative entries is at most the sum over all functions, which factorizes into the product of the row sums. This absorbs the factorial cardinality of a pure-cross fibre into m window rows.

The multi-window majorant

noncomputable def Anderson4D.r324LedgerThreeCrossMajorant (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : ℝ

The row-sum multi-window majorant: one full covariance row per left single. Each row is one diagonal-window sum in the remaining frequency estimate.

Equations

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

theorem Anderson4D.r324LedgerThreeCrossMajorant_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : 0 ≤ r324LedgerThreeCrossMajorant ρ ε m v

The multi-window majorant is nonnegative.

def Anderson4D.r324LedgerThreePermEntities (m : ℕ) : Finset (MomentContraction m)

The finset of all permutation entities ⟨id, id, π⟩.

Equations

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

theorem Anderson4D.r324LedgerThree_subset_permEntities {m : ℕ} {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) : F ⊆ r324LedgerThreePermEntities m

Every set of pure-cross entities embeds into the permutation entities.

theorem Anderson4D.r324LedgerThree_sum_permEntities {m : ℕ} (G : MomentContraction m → ℝ) : ∑ e ∈ r324LedgerThreePermEntities m, G e = ∑ π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles, G ⟨PartialPairing.id, ⟨PartialPairing.id, π⟩⟩

The permutation-entity sum of any function is the bijection sum.

theorem Anderson4D.r324LedgerThree_sum_permEntities_cross (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : ∑ e ∈ r324LedgerThreePermEntities m, momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd v = ∑ π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles, momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π v

Bijection-sum form of the permutation-entity covariance sum.

theorem Anderson4D.r324LedgerThree_sum_equiv_cross_le (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (v : Fin (2 * m) → T4) : ∑ π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles, momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π v ≤ r324LedgerThreeCrossMajorant ρ ε m v

Permanent bound for the full bijection sum.

theorem Anderson4D.r324LedgerThree_sum_crossCovariance_le (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (F : Finset (MomentContraction m)) (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) (v : Fin (2 * m) → T4) : ∑ e ∈ F, momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd v ≤ r324LedgerThreeCrossMajorant ρ ε m v

The permutation-summed cross covariance obeys the permanent bound: any set of pure-cross entities sums pointwise below the product of the m covariance row sums.

The pure-cross physical density

noncomputable def Anderson4D.r324LedgerThreeLeftChain (m : ℕ) (p : R324PhysicalPoint m) : ℝ

The plain left half chain of a pure-cross fibre.

Equations

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

noncomputable def Anderson4D.r324LedgerThreeRightChain (m : ℕ) (p : R324PhysicalPoint m) : ℝ

The plain right half chain of a pure-cross fibre.

Equations

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

theorem Anderson4D.r324LedgerThreeLeftChain_nonneg (m : ℕ) (p : R324PhysicalPoint m) : 0 ≤ r324LedgerThreeLeftChain m p

theorem Anderson4D.r324LedgerThreeRightChain_nonneg (m : ℕ) (p : R324PhysicalPoint m) : 0 ≤ r324LedgerThreeRightChain m p

noncomputable def Anderson4D.r324LedgerThreeCrossDensity (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : ℝ

The pure-cross fibre density: two plain Green chains times the still-summed (cancellation-free, nonnegative) cross covariance of the fibre.

Equations

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

theorem Anderson4D.r324LedgerThreeCrossDensity_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (F : Finset (MomentContraction m)) (p : R324PhysicalPoint m) : 0 ≤ r324LedgerThreeCrossDensity ρ ε m F p

theorem Anderson4D.r324LedgerThreeCrossDensity_le_majorant (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) (p : R324PhysicalPoint m) : r324LedgerThreeCrossDensity ρ ε m F p ≤ r324LedgerThreeLeftChain m p * r324LedgerThreeRightChain m p * r324LedgerThreeCrossMajorant ρ ε m p.2.2.2.2

Pointwise multi-window domination of the pure-cross density. The permanent bound replaces the factorial permutation sum by the product of the m covariance row sums.

Pointwise factorization of the flat pure-cross fibre

theorem Anderson4D.r324LedgerThree_flatten_allCross_eq (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) {e : MomentContraction m} (he : R324LedgerThreeAllCrossEntity e) (p : R324PhysicalPoint m) : r324Flatten (deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p = charT4 α p.1 * charT4 β p.2.1 * charT4 (-α) p.2.2.1 * charT4 (-β) p.2.2.2.1 * ↑(r324LedgerThreeLeftChain m p * r324LedgerThreeRightChain m p * momentCrossCovarianceProduct ρ ε m e.fst e.snd.fst e.snd.snd p.2.2.2.2)

One pure-cross flat integrand: external phase times plain chains times its cross covariance.

theorem Anderson4D.r324LedgerThree_norm_sum_flatten_eq (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (α β : Z4) {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) (p : R324PhysicalPoint m) : ‖∑ e ∈ F, r324Flatten (deterministicMomentIntegrand ρ ε m α β e.fst e.snd.fst e.snd.snd) p‖ = r324LedgerThreeCrossDensity ρ ε m F p

Exact norm of the summed pure-cross flat fibre: the phase has modulus one and everything else is nonnegative, so no cancellation and no triangle inequality is involved.

The summed pure-cross fibre as one nonnegative integral

theorem Anderson4D.r324LedgerThree_norm_termSum_le_integral_crossDensity (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (hfib : R324LedgerThreeCrossFibre m s r) : ‖momentRefinedDeterministicTermSum ρ ε m α β s r‖ ≤ ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m (momentRefinedContractionFiber m s r) p ∂r324PhysicalMeasure m

Cancellation-free integral bound for a pure-cross fibre. The summed fibre is one physical integral of the nonnegative pure-cross density; only the unimodular phase is discarded. Together with the pointwise permanent bound this reduces the cross-case ledger to the multi-window estimate for two plain chains against the row-sum majorant.