Grouped majorant after the four endpoint integrations

The four external Fourier variables have already been integrated in endpointIntegratedResidualDensity. This file bounds the two resulting boundary coefficients by their stored terminal edge scales and bounds only the two signed endpoint-erased Green chains. The complete residual primitive-pairing sum remains grouped throughout.

theorem Anderson4D.R324WithinHalfResidualPrefix.ae_endpointErased_edgeDisplacement_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : ∀ᵐ (v : res.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure, ∀ edge ∈ res.endpointErasedActiveEdgeSlots hactive, res.edgeDisplacement 0 0 (res.reconstruct v) edge ≠ 0

Every endpoint-erased terminal edge is off-diagonal almost everywhere on the surviving-coordinate product.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.endpointErasedInvSqChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (v : res.SurvivingCoordinate → T4) : ℝ

The endpoint-erased inverse-square path on one terminal half.

Equations

• res.endpointErasedInvSqChainProduct hactive v = ∏ edge ∈ res.endpointErasedActiveEdgeSlots hactive, Anderson4D.invSqKer (res.edgeDisplacement 0 0 (res.reconstruct v) edge)

theorem Anderson4D.R324WithinHalfResidualPrefix.endpointErasedInvSqChainProduct_nonneg {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (v : res.SurvivingCoordinate → T4) : 0 ≤ res.endpointErasedInvSqChainProduct hactive v

theorem Anderson4D.r324ResidualPrimitiveSumProduct_nonneg {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : 0 ≤ r324ResidualPrimitiveSumProduct ρ ε κp κm π v

The complete residual primitive-pairing sum is nonnegative. This allows its complex norm to be removed without splitting the finite sum.

noncomputable def Anderson4D.R324TwoHalfTerminalData.endpointIntegratedGroupedMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (π : ↥κp.singles ≃ ↥κm.singles) (p : (terminal.left.SurvivingCoordinate → T4) × (terminal.right.SurvivingCoordinate → T4)) : ℝ

The grouped positive majorant after the four external Fourier integrations. It contains every certified active-edge scale, four copies of the inverse-square mass, the two endpoint-erased inverse-square paths, and the complete residual primitive sum as one factor.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.norm_endpointIntegratedResidualDensity_le_groupedMajorant_of_offDiagonal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)) (hneLeft : ∀ edge ∈ leftTrace.terminalPrefix.endpointErasedActiveEdgeSlots hleft, leftTrace.terminalPrefix.edgeDisplacement 0 0 (leftTrace.terminalPrefix.reconstruct p.1) edge ≠ 0) (hneRight : ∀ edge ∈ rightTrace.terminalPrefix.endpointErasedActiveEdgeSlots hright, rightTrace.terminalPrefix.edgeDisplacement 0 0 (rightTrace.terminalPrefix.reconstruct p.2) edge ≠ 0) : let terminal := ofCertifiedTraces leftTrace rightTrace; ‖terminal.endpointIntegratedResidualDensity π hleft hright α β p‖ ≤ terminal.endpointIntegratedGroupedMajorant leftTrace.terminalScale rightTrace.terminalScale hleft hright π p

Pointwise grouped bound under the literal off-diagonal hypotheses for the two endpoint-erased paths.

theorem Anderson4D.R324TwoHalfTerminalData.ae_norm_endpointIntegratedResidualDensity_le_groupedMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) : let terminal := ofCertifiedTraces leftTrace rightTrace; (fun (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)) => ‖terminal.endpointIntegratedResidualDensity π hleft hright α β p‖) ≤ᵐ[(MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : rightTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure)] fun (p : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) × (rightTrace.terminalPrefix.SurvivingCoordinate → T4)) => terminal.endpointIntegratedGroupedMajorant leftTrace.terminalScale rightTrace.terminalScale hleft hright π p

Terminal-product version of the grouped majorant. All diagonal exceptions have been removed under the product Haar measure.

noncomputable def Anderson4D.R324TwoHalfTerminalData.initialNestedEndpointIntegratedGroupedMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData ρ lam ε κp κm) (leftScale rightScale : Fin (m + 1) → ℝ) (hleft : terminal.left.state.active.Nonempty) (hright : terminal.right.state.active.Nonempty) (π : ↥κp.singles ≃ ↥κm.singles) (v : terminal.NestedCoordinate π → T4) : ℝ

Pullback of the grouped majorant to the literal initial nested-cross carrier.

Equations

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

theorem Anderson4D.R324TwoHalfTerminalData.ae_norm_initialNestedEndpointIntegratedResidualDensity_le_groupedMajorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {leftRes : R324WithinHalfResidualPrefix ρ lam ε κp} {rightRes : R324WithinHalfResidualPrefix ρ lam ε κm} {leftInitialScale rightInitialScale : Fin (m + 1) → ℝ} (leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale) (rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale) (π : ↥κp.singles ≃ ↥κm.singles) (hleft : leftTrace.terminalPrefix.state.active.Nonempty) (hright : rightTrace.terminalPrefix.state.active.Nonempty) (α β : Z4) : let terminal := ofCertifiedTraces leftTrace rightTrace; (fun (v : terminal.NestedCoordinate π → T4) => ‖terminal.initialNestedEndpointIntegratedResidualDensity π hleft hright α β v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure] fun (v : terminal.NestedCoordinate π → T4) => terminal.initialNestedEndpointIntegratedGroupedMajorant leftTrace.terminalScale rightTrace.terminalScale hleft hright π v

Initial-nested-carrier form of the endpoint-integrated grouped bound. It is the terminal-product theorem transported by the exact measure-preserving two-half/nested reindexing.