Canonical route packages for the common-left Fourier move

Paper: R-324 — §4.2 Step 4(B), canonical common-left route package

This file contains only the route-independent seams needed after the four literal endpoint operations have finished. It retains evaluation linearity on the right package, exposes the exact common-translation character carried by the completed left half, and identifies translation of the terminal cross coefficient with translation of its doubled residual root.

No norm or estimate is taken here.

The common-left projection on the extra Haar parameter

theorem Anderson4D.R324WithinHalfResidualPrefix.measurable_r324CommonLeftProjection (I : Type u_1) (J : Type u_2) [Fintype I] [Fintype J] : Measurable fun (q : T4 × (I → T4) × (J → T4)) => (r324CommonTranslate q.1 q.2.1, q.2.2)

Joint measurability of the map which translates the whole left terminal tuple and then forgets the translation parameter.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324CommonLeftProjectionSectionMeasurableEquiv (I : Type u_1) (J : Type u_2) [Fintype I] (a : T4) : (I → T4) × (J → T4) ≃ᵐ (I → T4) × (J → T4)

At a fixed common-left parameter, translation of the left tuple and the identity on the right tuple form a measurable equivalence of the completed terminal carrier.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324CommonLeftProjectionSectionMeasurableEquiv_apply (I : Type u_1) (J : Type u_2) [Fintype I] (a : T4) (p : (I → T4) × (J → T4)) : (r324CommonLeftProjectionSectionMeasurableEquiv I J a) p = (r324CommonTranslate a p.1, p.2)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324CommonLeftProjectionSection (I : Type u_1) (J : Type u_2) [Fintype I] [Fintype J] (a : T4) : MeasureTheory.MeasurePreserving (⇑(r324CommonLeftProjectionSectionMeasurableEquiv I J a)) ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure)) ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))

Every fixed common-left section preserves the product Haar measure. The outer Haar variable is deliberately handled by Tonelli below: since the paper measure is not normalized, forgetting it is not measure-preserving.

theorem Anderson4D.R324WithinHalfResidualPrefix.quasiMeasurePreserving_r324CommonLeftProjection (I : Type u_1) (J : Type u_2) [Fintype I] [Fintype J] : MeasureTheory.Measure.QuasiMeasurePreserving (fun (q : T4 × (I → T4) × (J → T4)) => (r324CommonTranslate q.1 q.2.1, q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))) ((MeasureTheory.Measure.pi fun (x : I) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : J) => paperMeasure))

The joint projection is nonsingular. This is the precise replacement for the false measure-preserving claim one would get by forgetting the finite-mass outer Haar variable: null sets pull back to null sets because every fixed common-left section preserves terminal product Haar.

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.toLinear {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 : R324PaperRightRouteExactPackage left rightRoute) : R324PaperRightRouteExactLinearPackage left rightRoute

The completed right route already contains exactly the two evaluation laws required by the common-left coefficient factorization.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.toLinear left right = { package := right, densityEvaluationLinear := ⋯ }

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperRightRouteExactPackage.exists_linear_of_route {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) (hsingles : e0.snd.fst.singles.Nonempty) (route : R324PaperHalfEndpointRoute rightProviders) : Nonempty (R324PaperRightRouteExactLinearPackage left route)

Literal four-case producer for the right linear package.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.unitDensity_commonTranslate {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) (a : T4) (v : left.bound.carrier.SurvivingCoordinate → T4) : left.bound.density (fun (x : left.bound.carrier.SurvivingCoordinate → T4) => 1) beta (r324CommonTranslate a v) = charT4 (alpha + beta) a * left.bound.density (fun (x : left.bound.carrier.SurvivingCoordinate → T4) => 1) beta v

The common-translation covariance stored by every completed left route, in the exact form consumed by the abstract Haar-averaging theorem.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.crossCoefficient_commonTranslate_eq_leftInternalTranslate {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) (leftPost : left.bound.carrier.SurvivingCoordinate → T4) (rightPost : right.package.bound.carrier.SurvivingCoordinate → T4) (a : T4) : left.bound.crossCoefficient right.package.bound e0.snd.snd (r324CommonTranslate a leftPost) rightPost = ↑(r324ResidualPrimitiveSumProduct rho eps e0.fst e0.snd.fst e0.snd.snd ((r324LeftInternalTranslateMeasurableEquiv m a) (r324TwoHalfRootDoubledReconstruct left.bound.carrier right.package.bound.carrier (leftPost, rightPost))))

Translating every surviving coordinate of the completed left carrier is exactly translation of the left half of the doubled residual root. The primitive sum is compared only on momentResidualActive, its genuine support.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.integrable_commonLeft_crossCoefficient {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) : MeasureTheory.Integrable (fun (q : T4 × (left.bound.carrier.SurvivingCoordinate → T4) × (right.package.bound.carrier.SurvivingCoordinate → T4)) => charT4 (alpha + beta) q.1 * left.bound.crossCoefficient right.package.bound e0.snd.snd (r324CommonTranslate q.1 q.2.1) q.2.2 * (left.bound.density (fun (x : left.bound.carrier.SurvivingCoordinate → T4) => 1) beta q.2.1 * right.package.bound.density (fun (x : right.package.bound.carrier.SurvivingCoordinate → T4) => 1) (-beta) q.2.2)) (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : left.bound.carrier.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : right.package.bound.carrier.SurvivingCoordinate) => paperMeasure)))

The extra common-left Haar parameter is jointly integrable for the genuine residual cross coefficient. Pointwise, the displayed integrand is the already-integrable completed endpoint density composed with the common-left projection above.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperLeftRouteExactPackage.integral_nestedEndpointProductDensity_eq_commonLeftFourier {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) : (∫ (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) = ∫ (v : (left.bound.twoHalfTerminal right.package.bound).NestedCoordinate e0.snd.snd → T4), left.bound.nestedEndpointProductDensityWithCoefficient right.package.bound beta e0.snd.snd (r324CommonLeftFourierCoefficient (alpha + beta) (left.bound.crossCoefficient right.package.bound e0.snd.snd)) v ∂MeasureTheory.Measure.pi fun (x : (left.bound.twoHalfTerminal right.package.bound).NestedCoordinate e0.snd.snd) => paperMeasure

Canonical signed common-left Fourier identity on the initial nested carrier. All four endpoint operations and the exact two-half collapse have already happened before this equality; no absolute value occurs.