The genuine refined root after the direct incoming Fourier operation

This is the product-space version of the first endpoint operation in paper Step 4(A). The physical root is regrouped so that the incoming endpoint is the last variable. Joint integrability is inherited from the genuine refined physical fibre; only then is the one-variable Fourier identity from R324DirectIncomingInitialFourier applied sectionwise.

No norm or endpoint estimate occurs here.

Root regrouping

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324DirectIncomingRootMeasurableEquiv (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaP kappaM : PartialPairing (Fin m)) : R324PhysicalPoint m ≃ᵐ (R324IncomingExceptionalRootParameter rho lam eps kappaM × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)) × T4

Move the physical incoming endpoint behind the two initial residual carriers: (x,y,z,w,v) ↦ ((((y,z,w),v₋),v₊),x).

The first component before the last x is exactly the parameter order used by the direct-incoming source of the one-half transform.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324DirectIncomingRootMeasurableEquiv_apply (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaP kappaM : PartialPairing (Fin m)) (q : R324PhysicalPoint m) : (r324DirectIncomingRootMeasurableEquiv rho lam eps kappaP kappaM) q = ((((q.2.1, q.2.2.1, q.2.2.2.1), ((r324InitialTwoHalfProductPiMeasurableEquiv rho lam eps kappaP kappaM).symm q.2.2.2.2).2), ((r324InitialTwoHalfProductPiMeasurableEquiv rho lam eps kappaP kappaM).symm q.2.2.2.2).1), q.1)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324DirectIncomingRootMeasurableEquiv (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaP kappaM : PartialPairing (Fin m)) : MeasureTheory.MeasurePreserving (⇑(r324DirectIncomingRootMeasurableEquiv rho lam eps kappaP kappaM)) (r324PhysicalMeasure m) (((r324IncomingExceptionalRootParameterMeasure rho lam eps kappaM).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure)).prod paperMeasure)

The direct-incoming root regrouping preserves the literal product Haar measure.

The direct source on the regrouped root

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.directIncomingRefinedRootOuter (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaP kappaM : PartialPairing (Fin m)) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (omega : R324IncomingExceptionalRootParameter rho lam eps kappaM) (v : (initial rho lam eps kappaP).SurvivingCoordinate → T4) : ℂ

All factors of a refined root other than the incoming left character and incoming left Green leg.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.r324Flatten_momentRefinedPhysicalIntegrand_eq_directIncoming_reindex {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (alpha beta : Z4) (q : R324PhysicalPoint m) : r324Flatten (momentRefinedPhysicalIntegrand rho eps m alpha beta ↑p.fst ↑p.snd) q = charT4 alpha q.1 * (↑((initial rho lam eps e0.fst).residualIntegrand rho eps q.1 q.2.1 ((initial rho lam eps e0.fst).reconstruct ((r324InitialTwoHalfProductPiMeasurableEquiv rho lam eps e0.fst e0.snd.fst).symm q.2.2.2.2).1)) * directIncomingRefinedRootOuter rho lam eps e0.fst e0.snd.fst alpha beta e0.snd.snd ((q.2.1, q.2.2.1, q.2.2.2.1), ((r324InitialTwoHalfProductPiMeasurableEquiv rho lam eps e0.fst e0.snd.fst).symm q.2.2.2.2).2) ((r324InitialTwoHalfProductPiMeasurableEquiv rho lam eps e0.fst e0.snd.fst).symm q.2.2.2.2).1)

The regrouped genuine refined density is the raw initial left residual times the untouched root outer factor.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.directIncomingRefinedInitialSourceDensity (rho : SmoothCutoff) (lam eps : ℝ) {m : ℕ} (kappaP kappaM : PartialPairing (Fin m)) (alpha beta : Z4) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (q : R324IncomingExceptionalRootParameter rho lam eps kappaM × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)) : ℂ

The exact direct-incoming source density on the root parameter and initial left carrier.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_and_r324RefinedPhysicalIntegral_eq_directIncomingSource {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} (p : R324RefinedScheduleIndex m) (e0 : MomentContraction m) (he0 : e0 ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : MeasureTheory.Integrable (directIncomingRefinedInitialSourceDensity rho lam eps e0.fst e0.snd.fst alpha beta e0.snd.snd) ((r324IncomingExceptionalRootParameterMeasure rho lam eps e0.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.fst).SurvivingCoordinate) => paperMeasure)) ∧ r324RefinedPhysicalIntegral rho eps m alpha beta p = ∫ (q : R324IncomingExceptionalRootParameter rho lam eps e0.snd.fst × ((initial rho lam eps e0.fst).SurvivingCoordinate → T4)), directIncomingRefinedInitialSourceDensity rho lam eps e0.fst e0.snd.fst alpha beta e0.snd.snd q ∂(r324IncomingExceptionalRootParameterMeasure rho lam eps e0.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps e0.fst).SurvivingCoordinate) => paperMeasure)

The direct incoming operation on the genuine refined root. It returns both the integrability license required by the one-half transform and the exact signed integral identity.