Integrated Fourier terms for residual-refined R-324 cores

This module turns the pointwise common-increment grouping into the exact endpoint-first configuration series required by R324ConcreteRefinedCoreExpansion.

The physical product measure is stored in the order (x,y,z,w,v), while the grouped endpoint term integrates the internal tuple v first. We therefore construct the actual measure-preserving cyclic permutation and use joint integrability before changing the order of integration.

Moving the internal tuple in front of the four endpoints

@[reducible, inline]

abbrev Anderson4D.R324EndpointPoint : Type

The four external variables in their frozen order.

Equations

• Anderson4D.R324EndpointPoint = (Anderson4D.T4 × Anderson4D.T4 × Anderson4D.T4 × Anderson4D.T4)

noncomputable def Anderson4D.r324EndpointMeasure : MeasureTheory.Measure R324EndpointPoint

Product measure on the four external variables.

Equations

• Anderson4D.r324EndpointMeasure = Anderson4D.paperMeasure.prod (Anderson4D.paperMeasure.prod (Anderson4D.paperMeasure.prod Anderson4D.paperMeasure))

noncomputable def Anderson4D.r324InternalFirstMeasurableEquiv (m : ℕ) : R324PhysicalPoint m ≃ᵐ (Fin (2 * m) → T4) × R324EndpointPoint

Cyclic permutation (x,y,z,w,v) ↦ (v,x,y,z,w) of the physical product space.

Equations

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

@[simp]

theorem Anderson4D.r324InternalFirstMeasurableEquiv_apply {m : ℕ} (p : R324PhysicalPoint m) : (r324InternalFirstMeasurableEquiv m) p = (p.2.2.2.2, p.1, p.2.1, p.2.2.1, p.2.2.2.1)

theorem Anderson4D.measurePreserving_r324InternalFirstMeasurableEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324InternalFirstMeasurableEquiv m)) (r324PhysicalMeasure m) ((MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure).prod r324EndpointMeasure)

theorem Anderson4D.r324_integral_product_eq_internal_first {m : ℕ} (f : T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (hf : MeasureTheory.Integrable (r324Flatten f) (r324PhysicalMeasure m)) : ∫ (p : R324PhysicalPoint m), r324Flatten f p ∂r324PhysicalMeasure m = ∫ (v : Fin (2 * m) → T4), ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), f x y z w v ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Joint integrability licenses the endpoint-first integration order used by r324GroupedEndpointConfigurationTerm.

Raw refined endpoint configurations

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) (v : Fin (2 * m) → T4) : ℂ

Interior core of one ungrouped refined contraction/configuration.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Endpoint-separated physical integrand of one ungrouped refined configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawEndpointIntegrand_eq_fullPairing (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v = have u := (r324NatEquivRefinedContractionConfigurations p) a; have κ := (momentContractionEquivFullPairing m) ↑u.1; ρ.r324FullPairingFourierIntegrand ε α β κ (r324FullConfigurationOfStandard κ ((r324NatEquivStandardConfigurations hm) u.2)) x y z w v

One raw refined endpoint integrand is exactly the already-integrable full-pairing Fourier integrand selected by its contraction/configuration index.

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_refinedRawEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) : MeasureTheory.Integrable (r324Flatten (ρ.r324RefinedRawEndpointIntegrand hm ε α β p a)) (r324PhysicalMeasure m)

Every raw refined endpoint integrand is jointly integrable on the genuine five-group physical product space.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawEndpointL1 (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) : ℝ

Physical L¹ mass of one raw refined configuration.

Equations

• ρ.r324RefinedRawEndpointL1 hm ε α β p a = ∫ (q : Anderson4D.R324PhysicalPoint m), ‖Anderson4D.r324Flatten (ρ.r324RefinedRawEndpointIntegrand hm ε α β p a) q‖ ∂Anderson4D.r324PhysicalMeasure m

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawEndpointL1 (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) : Summable (ρ.r324RefinedRawEndpointL1 hm ε α β p)

The raw configurations in one whole refined fibre have summable physical L¹ masses.

Common-increment grouped endpoint integrands

theorem Anderson4D.SmoothCutoff.r324EndpointSeparatedIntegrand_tsumByKey {K : Type u_1} (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℕ → ℂ) (key : ℕ → K) (k : K) (x y z w : T4) : r324EndpointSeparatedIntegrand α β anchors flags (tsumByKey core key k) x y z w = tsumByKey (fun (a : ℕ) => r324EndpointSeparatedIntegrand α β anchors flags (core a) x y z w) key k

An endpoint-separated integrand commutes with a summable fibrewise tsum, because its dependence on the supplied core is linear.

theorem Anderson4D.SmoothCutoff.r324KeyGroupedRefinedEndpointCore_eq_tsumByKey (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) (v : Fin (2 * m) → T4) : ρ.r324KeyGroupedRefinedEndpointCore hm ε p b v = tsumByKey (fun (x : ℕ) => ρ.r324RefinedRawEndpointCore hm ε p x v) (r324RefinedRawIncrementKey hm p) ((r324NatEquivStandardConfigurations hm) b)

The key-grouped endpoint core is the fibrewise tsum of the raw endpoint cores sharing that increment vector.

noncomputable def Anderson4D.SmoothCutoff.r324KeyGroupedRefinedEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Endpoint-separated physical integrand of one common-increment group.

Equations

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

theorem Anderson4D.SmoothCutoff.r324KeyGroupedRefinedEndpointIntegrand_eq_tsumByKey (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324KeyGroupedRefinedEndpointIntegrand hm ε α β p b x y z w v = tsumByKey (fun (a : ℕ) => ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v) (r324RefinedRawIncrementKey hm p) ((r324NatEquivStandardConfigurations hm) b)

Pointwise common-increment grouping. The complete compatible primitive fibre is formed inside this tsum before any integral or norm.

Summable scalar majorants for the grouped series

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRawCovarianceWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) : ℝ

Coordinate-independent absolute covariance weight of one raw refined configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedRawCovarianceWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) : 0 ≤ ρ.r324RefinedRawCovarianceWeight hm ε p a

theorem Anderson4D.SmoothCutoff.norm_r324RefinedRawCovarianceConfiguration (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) (v : Fin (2 * m) → T4) : ‖ρ.r324RefinedRawCovarianceConfiguration hm ε p a v‖ = ρ.r324RefinedRawCovarianceWeight hm ε p a

theorem Anderson4D.SmoothCutoff.summable_r324RefinedRawCovarianceWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) : Summable (ρ.r324RefinedRawCovarianceWeight hm ε p)

noncomputable def Anderson4D.SmoothCutoff.r324RefinedRepresentativeBare {m : ℕ} (p : R324RefinedScheduleIndex m) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Common two-skeleton factor of a whole refined fibre.

Equations

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

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_refinedRepresentativeBare {m : ℕ} (p : R324RefinedScheduleIndex m) : MeasureTheory.Integrable (r324Flatten (r324RefinedRepresentativeBare p)) (r324PhysicalMeasure m)

theorem Anderson4D.SmoothCutoff.norm_r324RefinedRawEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ‖ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v‖ = ‖r324RefinedRepresentativeBare p x y z w v‖ * ρ.r324RefinedRawCovarianceWeight hm ε p a

Exact pointwise norm separation into the common physical skeleton and the coordinate-independent covariance weight.

Integrability of every common-increment group

noncomputable def Anderson4D.SmoothCutoff.r324KeyGroupedRefinedCovarianceWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) : ℝ

Scalar covariance budget of one common-increment group.

Equations

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

theorem Anderson4D.SmoothCutoff.r324KeyGroupedRefinedCovarianceWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (b : ℕ) : 0 ≤ ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p b

theorem Anderson4D.SmoothCutoff.summable_r324KeyGroupedRefinedCovarianceWeight (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) : Summable (ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p)

theorem Anderson4D.SmoothCutoff.norm_r324KeyGroupedRefinedEndpointIntegrand_le (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (x y z w : T4) (v : Fin (2 * m) → T4) : ‖ρ.r324KeyGroupedRefinedEndpointIntegrand hm ε α β p b x y z w v‖ ≤ ‖r324RefinedRepresentativeBare p x y z w v‖ * ρ.r324KeyGroupedRefinedCovarianceWeight hm ε p b

Pointwise norm bound by the common two-skeleton factor and the scalar weight of the whole increment group.

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_keyGroupedRefinedEndpointIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) : MeasureTheory.Integrable (r324Flatten (ρ.r324KeyGroupedRefinedEndpointIntegrand hm ε α β p b)) (r324PhysicalMeasure m)

Every common-increment group is jointly integrable.