Complete nested run with a separate cross-covariance cutoff

Paper: R-324 — §4.2 Step 4(B), mixed-cutoff complete nested run

The terminal half traces remember the original cutoff used during the within-half elimination. After those eliminations, however, the grouped cross-block covariance product may be replaced by a positive analytic majorant built from a second cutoff. This file records that separation: the two inverse-square terminal chains are unchanged, while every complete primitive head in the nested cross run uses sigma.

noncomputable def Anderson4D.R324TwoHalfTerminalData.completeNestedRunDensityWithCrossCutoff {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) (v : step.SurvivingCoordinate → T4) : ℝ

The literal Steps 2--3 density with the terminal half geometry inherited from rho and the grouped cross covariance heads evaluated with sigma.

Equations

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

@[simp]

theorem Anderson4D.R324TwoHalfTerminalData.completeNestedRunDensityWithCrossCutoff_self {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : terminal.completeNestedRunDensityWithCrossCutoff rho step hleft hright = terminal.completeNestedRunDensity step hleft hright

theorem Anderson4D.R324TwoHalfTerminalData.completeNestedRunDensityWithCrossCutoff_nonneg {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) (v : step.SurvivingCoordinate → T4) : 0 ≤ terminal.completeNestedRunDensityWithCrossCutoff sigma step hleft hright v

Pointwise positivity does not require identifying a complete budget run.

theorem Anderson4D.R324TwoHalfTerminalData.ae_completeNestedRunDensityWithCrossCutoff_eq_head_connector_next {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) (ctx : R324NestedCrossProperStepContext kappaPlus kappaMinus pi) : terminal.completeNestedRunDensityWithCrossCutoff sigma ctx.step ⋯ ⋯ =ᵐ[MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure] fun (v : ctx.step.SurvivingCoordinate → T4) => ctx.step.completeNormalizedHeadDensity sigma lam eps (ctx.step.splitSurvivingPiMeasurableEquiv v).1 * ctx.connector (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (ctx.step.splitSurvivingPiMeasurableEquiv v).2 * terminal.completeNestedRunDensityWithCrossCutoff sigma ctx.nextContext ⋯ ⋯ fun (i : ctx.nextContext.SurvivingCoordinate) => (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ⟨↑i, ⋯⟩

One proper shell of the mixed-cutoff run. The terminal chains are geometric; only the complete grouped primitive head changes to sigma.

theorem Anderson4D.R324TwoHalfTerminalData.ae_completeNestedRunDensityWithCrossCutoff_eq_completeHeadPullback_of_tail_eq_nil {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (htail : step.tail = []) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : terminal.completeNestedRunDensityWithCrossCutoff sigma step hleft hright =ᵐ[MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure] step.completeHeadPullbackDensity sigma lam eps

At the final shell, the mixed density is the complete sigma head pulled back to the surviving coordinates.

theorem Anderson4D.R324TwoHalfTerminalData.integrable_completeNestedRunDensityWithCrossCutoff_at_truncation {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hmtrunc : m ≤ truncOrder eps) (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : MeasureTheory.Integrable (terminal.completeNestedRunDensityWithCrossCutoff sigma step hleft hright) (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure)

Integrability of the mixed run follows by the same literal shell recursion as the original run, with the proper-head provider chosen from sigma.

theorem Anderson4D.R324TwoHalfTerminalData.exists_prefix_terminal_integral_completeNestedRunDensityWithCrossCutoff_le {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus) (sigma : SmoothCutoff) {D : ℝ} (hlam : 0 < lam) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hmtrunc : m ≤ truncOrder eps) (provider : R324CompleteProperHeadSharpProvider sigma lam eps D kappaPlus kappaMinus pi) (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty) : ∃ (prefixOrder : ℕ) (terminalOrder : ℕ) (finalStep : R324NestedCrossStepContext kappaPlus kappaMinus pi), step.residual.remainingOrder = prefixOrder + terminalOrder ∧ terminalOrder = finalStep.order ∧ (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensityWithCrossCutoff sigma step hleft hright v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ (D * lam) ^ (2 * prefixOrder) * ∫ (t : Fin (2 * finalStep.order) → T4), finalStep.completeNormalizedHeadDensity sigma lam eps t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * finalStep.order)) => paperMeasure

Quantitative shell removal for the mixed-cutoff density.

theorem Anderson4D.R324TwoHalfTerminalData.exists_integral_completeNestedRunDensityWithCrossCutoff_le_primitiveInsertedMajorant (sigma : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaPlus kappaMinus : PartialPairing (Fin m)} {pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles} (terminal : R324TwoHalfTerminalData rho lam eps kappaPlus kappaMinus), 0 < lam → 0 < eps → eps ≤ 1 → 1 ≤ |Real.log eps| → m ≤ truncOrder eps → ∀ (step : R324NestedCrossStepContext kappaPlus kappaMinus pi) (hleft : (r324LeftHalfPullback step.residual.activeCarrier).Nonempty) (hright : (r324RightHalfPullback step.residual.activeCarrier).Nonempty), (∫ (v : step.SurvivingCoordinate → T4), terminal.completeNestedRunDensityWithCrossCutoff sigma step hleft hright v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant C lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure

Uniform mixed-cutoff closure. The constants depend only on the analytic cross cutoff sigma; the terminal half geometry may come from an arbitrary original cutoff rho.