Common-left Fourier averaging after the endpoint collapse

Paper: R-324 — §4.2 Step 4(B), common-left Fourier averaging

Paper Step 4(B) takes its common translation only after all four endpoint operations have been completed. This file isolates the two formal facts needed at that point:

• a coefficient-parametric endpoint density factors pointwise through the value of the coefficient at the surviving terminal tuple, provided the two already-completed half densities have their literal evaluation-linearity;
• a common translation of a finite torus tuple preserves product Haar, and a covariant unit density may consequently be averaged into the corresponding common-left Fourier coefficient.

The statements are deliberately independent of the sixteen endpoint cases. Canonical route packages can supply the small evaluation-law wrapper from their existing density_mul and density_congr_at proofs. No norm is taken in this file.

Common translation on a finite terminal carrier

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslate {I : Type u_1} (a : T4) (v : I → T4) : I → T4

Translate every coordinate of a finite torus tuple by the same point.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslate a v i = v i + a

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslate_apply {I : Type u_1} (a : T4) (v : I → T4) (i : I) : r324CommonTranslate a v i = v i + a

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslateMeasurableEquiv (I : Type u_1) (a : T4) : (I → T4) ≃ᵐ (I → T4)

The common translation as a measurable equivalence.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslateMeasurableEquiv I a = MeasurableEquiv.piCongrRight fun (x : I) => MeasurableEquiv.addRight a

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324CommonTranslateMeasurableEquiv_apply {I : Type u_1} (a : T4) (v : I → T4) : (r324CommonTranslateMeasurableEquiv I a) v = r324CommonTranslate a v

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324CommonTranslate (I : Type u_1) [Fintype I] (a : T4) : MeasureTheory.MeasurePreserving (r324CommonTranslate a) (MeasureTheory.Measure.pi fun (x : I) => paperMeasure) (MeasureTheory.Measure.pi fun (x : I) => paperMeasure)

Product Haar is invariant under a common translation of all coordinates. The finite hypothesis is exactly the one available on every terminal surviving-coordinate type.

Evaluation-linearity of a completed half density

structure Anderson4D.R324WithinHalfResidualPrefix.R324EndpointDensityEvaluationLinear {I : Type u_1} (density : ((I → T4) → ℂ) → Z4 → (I → T4) → ℂ) : Prop

The only two algebraic laws used after a one-half endpoint route has finished. They are pointwise laws, not continuity or positivity data.

• mul (a : ℂ) (coefficient : (I → T4) → ℂ) (mode : Z4) (v : I → T4) : density (fun (u : I → T4) => a * coefficient u) mode v = a * density coefficient mode v
• congr_at (leftCoefficient rightCoefficient : (I → T4) → ℂ) (mode : Z4) (v : I → T4) : leftCoefficient v = rightCoefficient v → density leftCoefficient mode v = density rightCoefficient mode v

theorem Anderson4D.R324WithinHalfResidualPrefix.R324EndpointDensityEvaluationLinear.density_eq_value_mul_unit {I : Type u_1} {density : ((I → T4) → ℂ) → Z4 → (I → T4) → ℂ} (law : R324EndpointDensityEvaluationLinear density) (coefficient : (I → T4) → ℂ) (mode : Z4) (v : I → T4) : density coefficient mode v = coefficient v * density (fun (x : I → T4) => 1) mode v

At a fixed terminal tuple, a completed endpoint density only sees the value of its coefficient there.

The exact left route package already stores precisely these two laws.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.densityEvaluationLinear {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {leftRoute : R324PaperHalfEndpointRoute leftProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) : R324EndpointDensityEvaluationLinear left.bound.density

Evaluation-linearity of the left density, repackaged without changing the existing exact-route structure.

structure Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactLinearPackage {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (rightRoute : R324PaperHalfEndpointRoute rightProviders) : Type

A non-rippling wrapper for a right exact package that retains the two pointwise evaluation laws. Canonical route constructors can populate this wrapper while the old exact package, and hence its exact collapse theorem, remain unchanged.

• package : R324PaperRightRouteExactPackage left rightRoute
• densityEvaluationLinear : R324EndpointDensityEvaluationLinear self.package.bound.density

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactLinearPackage.exactCollapse_to_nested {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {alpha beta : Z4} {p : R324RefinedScheduleIndex m} {e0 : MomentContraction m} {leftProviders : R324PaperHalfRouteProviders e0.fst alpha} {rightProviders : R324PaperHalfRouteProviders e0.snd.fst (-alpha)} {leftRoute : R324PaperHalfEndpointRoute leftProviders} {rightRoute : R324PaperHalfEndpointRoute rightProviders} (left : R324PaperLeftRouteExactPackage p e0 leftRoute beta) (right : R324PaperRightRouteExactLinearPackage left rightRoute) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps e0.fst).remainingOrder + (initial rho lam eps e0.snd.fst).remainingOrder)) * r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (v : (left.bound.twoHalfTerminal right.package.bound).NestedCoordinate e0.snd.snd → T4), left.bound.nestedEndpointProductDensity right.package.bound beta e0.snd.snd v ∂MeasureTheory.Measure.pi fun (x : (left.bound.twoHalfTerminal right.package.bound).NestedCoordinate e0.snd.snd) => paperMeasure

The old exact collapse is inherited verbatim by the linear wrapper.

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.endpointUnitProductDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} {routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) (beta : Z4) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : ℂ

The unit endpoint product retained after all four endpoint operations.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.endpointProductDensityWithCoefficient_eq_coefficient_mul_unit {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} {routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) (leftLaw : R324EndpointDensityEvaluationLinear left.density) (rightLaw : R324EndpointDensityEvaluationLinear right.density) (beta : Z4) (coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ) (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) : left.endpointProductDensityWithCoefficient right beta coefficient p = coefficient p.1 p.2 * left.endpointUnitProductDensity right beta p

Exact pointwise factorization of the coefficient-parametric endpoint density. In particular, the complete signed coefficient is not split before the endpoint operations have finished.

Abstract common-left Fourier averaging

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324CommonLeftFourierCoefficient {I : Type u_1} {J : Type u_2} (mode : Z4) (coefficient : (I → T4) → (J → T4) → ℂ) (left : I → T4) (right : J → T4) : ℂ

The common-left Fourier coefficient of a two-terminal coefficient. The right terminal tuple is held fixed.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_coefficient_mul_covariantUnit_eq_commonLeftFourier {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] (mode : Z4) (leftUnit : (I → T4) → ℂ) (rightUnit : (J → T4) → ℂ) (coefficient : (I → T4) → (J → T4) → ℂ) (hcov : ∀ (a : T4) (v : I → T4), leftUnit (r324CommonTranslate a v) = charT4 mode a * leftUnit v) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (I → T4) × (J → T4)) => charT4 mode q.1 * coefficient (r324CommonTranslate q.1 q.2.1) q.2.2 * (leftUnit q.2.1 * rightUnit q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)))) : ∫ (p : (I → T4) × (J → T4)), coefficient p.1 p.2 * (leftUnit p.1 * rightUnit p.2) ∂(MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure) = ∫ (p : (I → T4) × (J → T4)), r324CommonLeftFourierCoefficient mode coefficient p.1 p.2 * (leftUnit p.1 * rightUnit p.2) ∂(MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)

Haar averaging at a covariant unit density. This is the exact abstract form of the common-left Fourier move in paper Step 4(B). The only analytic input is joint integrability before the Fubini exchange.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.integral_endpointProductDensityWithCoefficient_eq_commonLeftFourier {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} {routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) (leftLaw : R324EndpointDensityEvaluationLinear left.density) (rightLaw : R324EndpointDensityEvaluationLinear right.density) (beta : Z4) (coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ) (hcov : ∀ (a : T4) (v : left.carrier.SurvivingCoordinate → T4), left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta (r324CommonTranslate a v) = charT4 (alpha + beta) a * left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta v) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => charT4 (alpha + beta) q.1 * coefficient (r324CommonTranslate q.1 q.2.1) q.2.2 * (left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta q.2.1 * right.density (fun (x : right.carrier.SurvivingCoordinate → T4) => 1) (-beta) q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : ∫ (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)), left.endpointProductDensityWithCoefficient right beta coefficient p ∂(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure) = ∫ (p : (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)), left.endpointProductDensityWithCoefficient right beta (r324CommonLeftFourierCoefficient (alpha + beta) coefficient) p ∂(MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)

Replace the complete coefficient of the already-completed endpoint product by its common-left Fourier coefficient. This is a signed identity; the first norm may be taken only after this theorem.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.integral_nestedEndpointProductDensityWithCoefficient_eq_commonLeftFourier {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} {routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders} (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) (leftLaw : R324EndpointDensityEvaluationLinear left.density) (rightLaw : R324EndpointDensityEvaluationLinear right.density) (beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (coefficient : (left.carrier.SurvivingCoordinate → T4) → (right.carrier.SurvivingCoordinate → T4) → ℂ) (hcov : ∀ (a : T4) (v : left.carrier.SurvivingCoordinate → T4), left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta (r324CommonTranslate a v) = charT4 (alpha + beta) a * left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta v) (hjoint : MeasureTheory.Integrable (fun (q : T4 × (left.carrier.SurvivingCoordinate → T4) × (right.carrier.SurvivingCoordinate → T4)) => charT4 (alpha + beta) q.1 * coefficient (r324CommonTranslate q.1 q.2.1) q.2.2 * (left.density (fun (x : left.carrier.SurvivingCoordinate → T4) => 1) beta q.2.1 * right.density (fun (x : right.carrier.SurvivingCoordinate → T4) => 1) (-beta) q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.carrier.SurvivingCoordinate) => paperMeasure)))) : (∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), left.nestedEndpointProductDensityWithCoefficient right beta pi coefficient v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure) = ∫ (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4), left.nestedEndpointProductDensityWithCoefficient right beta pi (r324CommonLeftFourierCoefficient (alpha + beta) coefficient) v ∂MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure

The same common-left Fourier identity on the literal initial nested carrier used by the exact R-324 collapse.