Selected coefficient ledger after endpoint integration

After the four endpoint Fourier integrals have been evaluated, the remaining selected core contains only the two interior Green profiles and the fixed covariance configuration. This file separates its constant Fourier coefficient weight exactly.

noncomputable def Anderson4D.SmoothCutoff.r324SelectedInteriorSkeletonNormDensity {m : ℕ} (κp κm : PartialPairing (Fin m)) (v : Fin (2 * m) → T4) : ℝ

Bare norm of the two endpoint-independent Green profiles.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedInteriorSkeletonNormDensity_nonneg {m : ℕ} (κp κm : PartialPairing (Fin m)) (v : Fin (2 * m) → T4) : 0 ≤ r324SelectedInteriorSkeletonNormDensity κp κm v

theorem Anderson4D.SmoothCutoff.norm_r324SelectedEndpointCore_eq_weight_mul_interior (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (v : Fin (2 * m) → T4) : ‖ρ.r324SelectedEndpointCore ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ‖z4EuclideanFrequency (α + β)‖ v‖ = ‖ρ.covarianceModeCoeff ε (↑ω (r324CrossSlotPairIndex κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)))‖ * ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) * r324SelectedInteriorSkeletonNormDensity κp κm v

Exact norm separation for the endpoint-independent selected core. The canonical selector guarantee is used only to replace the guarded high factor by the original fixed Fourier factor.

noncomputable def Anderson4D.SmoothCutoff.r324SelectedInteriorSkeletonCellMass {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : ℝ

Bare interior-profile mass on one actual selected internal cell.

Equations

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

theorem Anderson4D.SmoothCutoff.r324SelectedInteriorSkeletonCellMass_nonneg {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) (cell : Fin (2 * m) → Z4) : 0 ≤ r324SelectedInteriorSkeletonCellMass κp κm π selected ε hε cell

theorem Anderson4D.SmoothCutoff.integral_norm_r324SelectedEndpointCore_on_cell (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (cell : Fin (2 * m) → Z4) : (∫ (v : Fin (2 * m) → T4) in r324SelectedInternalCell κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε cell, ‖ρ.r324SelectedEndpointCore ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ‖z4EuclideanFrequency (α + β)‖ v‖ ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ‖ρ.covarianceModeCoeff ε (↑ω (r324CrossSlotPairIndex κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)))‖ * ρ.r324SelectedUnselectedConfigurationWeight ε κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) * r324SelectedInteriorSkeletonCellMass κp κm π (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ε hε cell

Exact integral of the selected-core norm on one genuine internal cell.