Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324PaperEndpointCaseAssembly

The two actual endpoint branches #

The refined schedule has exactly the dichotomy used in paper Section 4.2: either a residual single survives in both halves, or every contraction in the refined fibre is full/full. This file is only the logical case split. All signed removals and endpoint integrations stay inside the two producer interfaces below.

source
def Anderson4D.R324PaperResidualEndpointWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) :
Prop

Step 4(A) after all signed removals in the residual branch.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Anderson4D.R324PaperFullEndpointWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) :
    Prop

    Step 4(A) after all signed removals in the full/full fibre branch.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Anderson4D.R324PaperFullEndpointZeroShiftWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) :
      Prop

      The only quantitative full/full endpoint calculation: at zero conserved shift the two full Step-1 halves supply the four ordinary-J sacrifices. The nonzero-shift case is Fourier orthogonality and is added below for free.

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

        Harmless enlargement of the primitive constant #

        source
        theorem Anderson4D.R324PaperResidualEndpointWeightedMajorantBound.mono_primitive {rho : SmoothCutoff} {C C' supportConstant : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (h : R324PaperResidualEndpointWeightedMajorantBound rho C supportConstant) :
        R324PaperResidualEndpointWeightedMajorantBound rho C' supportConstant

        The residual endpoint producer is monotone in its primitive constant. This lets independently constructed endpoint branches be joined by taking one maximum only after both paper-order proofs are complete.

        source
        theorem Anderson4D.R324PaperFullEndpointWeightedMajorantBound.mono_primitive {rho : SmoothCutoff} {C C' supportConstant : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (h : R324PaperFullEndpointWeightedMajorantBound rho C supportConstant) :
        R324PaperFullEndpointWeightedMajorantBound rho C' supportConstant

        The full/full endpoint producer is monotone in its primitive constant.

        source
        theorem Anderson4D.R324PaperFullEndpointZeroShiftWeightedMajorantBound.mono_primitive {rho : SmoothCutoff} {C C' supportConstant : ℝ} (hC : 0 ≤ C) (hCC' : C ≤ C') (h : R324PaperFullEndpointZeroShiftWeightedMajorantBound rho C supportConstant) :
        R324PaperFullEndpointZeroShiftWeightedMajorantBound rho C' supportConstant

        The zero-shift full/full endpoint producer is likewise monotone in its primitive constant.

        source
        theorem Anderson4D.R324PaperFullEndpointZeroShiftWeightedMajorantBound.toAllShift {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 ≤ primitiveConstant) (hzero : R324PaperFullEndpointZeroShiftWeightedMajorantBound rho primitiveConstant supportConstant) :
        R324PaperFullEndpointWeightedMajorantBound rho primitiveConstant supportConstant

        A zero-shift quantitative full/full producer already gives the arbitrary-shift full/full producer: a nonzero conserved Fourier mode vanishes exactly before any estimate.

        source
        theorem Anderson4D.R324PaperEndpointAllShiftWeightedMajorantBound.of_scheduleCases {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hresidual : R324PaperResidualEndpointWeightedMajorantBound rho primitiveConstant supportConstant) (hfull : R324PaperFullEndpointWeightedMajorantBound rho primitiveConstant supportConstant) :
        R324PaperEndpointAllShiftWeightedMajorantBound rho primitiveConstant supportConstant

        The residual/full dichotomy is exhaustive, so the two physical producers give the arbitrary-shift endpoint estimate with no additional analytic step.

        source
        theorem Anderson4D.R324PaperEndpointAllShiftWeightedMajorantBound.of_separateConstants {rho : SmoothCutoff} {residualConstant fullConstant supportConstant : ℝ} (hResidualConstant : 0 ≤ residualConstant) (hFullConstant : 0 ≤ fullConstant) (hresidual : R324PaperResidualEndpointWeightedMajorantBound rho residualConstant supportConstant) (hfull : R324PaperFullEndpointWeightedMajorantBound rho fullConstant supportConstant) :
        R324PaperEndpointAllShiftWeightedMajorantBound rho (max residualConstant fullConstant) supportConstant

        Independently produced residual and full/full constants can be merged at the final schedule case split.

        source
        theorem Anderson4D.R324PaperEndpointAllShiftWeightedMajorantBound.of_residual_and_zeroShift {rho : SmoothCutoff} {residualConstant fullConstant supportConstant : ℝ} (hResidualConstant : 0 ≤ residualConstant) (hFullConstant : 0 ≤ fullConstant) (hresidual : R324PaperResidualEndpointWeightedMajorantBound rho residualConstant supportConstant) (hzero : R324PaperFullEndpointZeroShiftWeightedMajorantBound rho fullConstant supportConstant) :
        R324PaperEndpointAllShiftWeightedMajorantBound rho (max residualConstant fullConstant) supportConstant

        Producer-facing version in which the full/full calculation is required only at zero conserved shift; Fourier orthogonality supplies all other full/full shifts before the two independent constants are merged.