Independent primitive coordinates of one refined R-324 fibre

Fixing the within-half and residual endpoint signatures fixes the complete primitive-block schedule. Every contraction in that refined fibre therefore embeds in the generic fibre of ambient pairings which are full and relatively primitive on every block. The carrier-generic product equivalence then reindexes the covariance sum by one independent primitive pairing coordinate per block.

The embedding may harmlessly enlarge the refined fibre. Since covariance products are nonnegative, this gives the exact direction needed by the integrated moment estimate without a pairing-cardinality factor.

@[reducible, inline]

abbrev Anderson4D.MomentRefinedContractionFiberAt (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) : Type

The finite type underlying one concrete residual-refined contraction fibre.

Equations

• Anderson4D.MomentRefinedContractionFiberAt m s r = ↥(Anderson4D.momentRefinedContractionFiber m s r)

def Anderson4D.momentRefinedFiberToPrimitivePartitionFiber {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (e : MomentRefinedContractionFiberAt m s r) : PrimitivePartitionFiber (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)

A member of a residual-refined fibre is full and relatively primitive on every block of the common schedule represented by e₀.

Equations

• Anderson4D.momentRefinedFiberToPrimitivePartitionFiber e₀ he₀ e = ⟨Anderson4D.momentCombinedPairing (↑e).fst (↑e).snd.fst (↑e).snd.snd, ⋯⟩

theorem Anderson4D.momentRefinedFiberToPrimitivePartitionFiber_injective {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : Function.Injective (momentRefinedFiberToPrimitivePartitionFiber e₀ he₀)

The common-schedule map is faithful because the complete doubled pairing uniquely determines the contraction triple.

noncomputable def Anderson4D.momentRefinedFiberPrimitiveCoordinatesEmbedding {m : ℕ} {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) : MomentRefinedContractionFiberAt m s r ↪ PrimitivePartitionCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)

The residual-refined fibre therefore injects into the exact dependent product of standard primitive-pairing coordinates, with no quotient and no multiplicity.

Equations

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

theorem Anderson4D.sum_refinedCovariance_le_sum_primitivePartitionFiber (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ∑ e : MomentRefinedContractionFiberAt m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing (↑e).fst (↑e).snd.fst (↑e).snd.snd) v ≤ ∑ τ : PrimitivePartitionFiber (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd), primitiveCovarianceProduct ρ ε m (↑τ) v

A nonnegative covariance sum over one refined fibre is bounded by the complete common primitive-partition fibre. This is an enlargement of the finite domain, not a termwise cardinality estimate.

theorem Anderson4D.sum_refinedCovariance_le_sum_primitivePartitionCoordinates (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v ≤ ∑ coordinates : PrimitivePartitionCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd), primitiveCovarianceProduct ρ ε m (↑((primitivePartitionFiberEquivCoordinates (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd)).symm coordinates)) v

Paper-facing form: the original finset sum is bounded by the dependent product of one primitive coordinate on each concrete block.

Exact covariance factorization of the enlarged fibre

noncomputable def Anderson4D.primitivePartitionBlockCovarianceFactor {n : ℕ} {κ : PartialPairing (Fin n)} (ρ : SmoothCutoff) (ε : ℝ) (P : PrimitiveBlockPartition κ) (B : PrimitivePartitionBlockIndex P) (σ : ↥(primitiveFullPairings (residualBlockOrder ↑B))) (v : Fin n → T4) : ℝ

The standard primitive covariance factor selected by one coordinate of a generic complete primitive partition.

Equations

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

theorem Anderson4D.pairingCovarianceProductOn_primitivePartitionFiber_eq_blockCoordinate {n : ℕ} {κ : PartialPairing (Fin n)} (ρ : SmoothCutoff) (ε : ℝ) (P : PrimitiveBlockPartition κ) (τ : PrimitivePartitionFiber P) (B : PrimitivePartitionBlockIndex P) (v : Fin n → T4) : pairingCovarianceProductOn ρ ε (↑τ) (↑B) v = primitivePartitionBlockCovarianceFactor ρ ε P B (primitivePartitionFiberCoordinates P τ B) v

The ambient covariance factor on one block is literally the standard primitive factor selected by that block's dependent coordinate.

theorem Anderson4D.primitiveBlockPartition_blocks_nodup {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : P.blocks.Nodup

Pairwise-disjoint nonempty blocks cannot repeat.

theorem Anderson4D.primitiveBlockPartition_list_prod_eq_fintype_prod {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {M : Type u_1} [CommMonoid M] (f : Finset (Fin n) → M) : (List.map f P.blocks).prod = ∏ B : PrimitivePartitionBlockIndex P, f ↑B

A list product over the concrete block schedule is the dependent fintype product over blocks with their membership certificates.

theorem Anderson4D.primitiveCovarianceProduct_primitivePartitionFiber_eq_prod_coordinates (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin (2 * m))) (P : PrimitiveBlockPartition κ) (τ : PrimitivePartitionFiber P) (v : Fin (2 * m) → T4) : primitiveCovarianceProduct ρ ε m (↑τ) v = ∏ B : PrimitivePartitionBlockIndex P, primitivePartitionBlockCovarianceFactor ρ ε P B (primitivePartitionFiberCoordinates P τ B) v

The full ambient covariance product is the product of the standard primitive covariance factors selected independently on all blocks.

theorem Anderson4D.sum_primitivePartitionFiber_covariance_eq_prod_primitiveSums (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin (2 * m))) (P : PrimitiveBlockPartition κ) (v : Fin (2 * m) → T4) : ∑ τ : PrimitivePartitionFiber P, primitiveCovarianceProduct ρ ε m (↑τ) v = ∏ B : PrimitivePartitionBlockIndex P, ∑ σ : ↥(primitiveFullPairings (residualBlockOrder ↑B)), primitivePartitionBlockCovarianceFactor ρ ε P B σ v

Summing the enlarged common-block fibre separates exactly into the product of the complete primitive-pairing sums on its blocks.

theorem Anderson4D.sum_refinedCovariance_le_prod_primitiveBlockSums (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) : ∑ e ∈ momentRefinedContractionFiber m s r, primitiveCovarianceProduct ρ ε m (momentCombinedPairing e.fst e.snd.fst e.snd.snd) v ≤ ∏ B : PrimitivePartitionBlockIndex (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd), ∑ σ : ↥(primitiveFullPairings (residualBlockOrder ↑B)), primitivePartitionBlockCovarianceFactor ρ ε (momentPrimitiveBlockPartition e₀.fst e₀.snd.fst e₀.snd.snd) B σ v

A realized refined covariance sum is controlled by the exact product of complete primitive sums on its common concrete block schedule.