Documentation

EpsilonEridani.QFT.Scattering.DIS.Corrections.Basic

Power Corrections Interfaces (Stage 12) #

This module defines target-mass and higher-twist correction interfaces and reduction lemmas to baseline LO observables.

source
@[reducible, inline]
abbrev EpsilonEridani.QFT.Scattering.DIS.Corrections.TargetMassCorrection :
Type

Target-mass correction term interface.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev EpsilonEridani.QFT.Scattering.DIS.Corrections.HigherTwistCorrection :
    Type

    Higher-twist correction term interface.

    Equations
    Instances For
      source
      def EpsilonEridani.QFT.Scattering.DIS.Corrections.correctedObservable (F : ℝ → ℝ → ℝ) (δTM : TargetMassCorrection) (δHT : HigherTwistCorrection) (x Q2 : ℝ) :
      ℝ

      Corrected observable decomposition into baseline + corrections.

      Equations
      Instances For
        source
        theorem EpsilonEridani.QFT.Scattering.DIS.Corrections.correctedObservable_decompose (F : ℝ → ℝ → ℝ) (δTM : TargetMassCorrection) (δHT : HigherTwistCorrection) (x Q2 : ℝ) :
        correctedObservable F δTM δHT x Q2 = F x Q2 + δTM x Q2 + δHT x Q2

        Decomposition identity for corrected observables.

        source
        theorem EpsilonEridani.QFT.Scattering.DIS.Corrections.correctedObservable_eq_baseline_of_zero (F : ℝ → ℝ → ℝ) (δTM : TargetMassCorrection) (δHT : HigherTwistCorrection) (x Q2 : ℝ) (hTM : δTM x Q2 = 0) (hHT : δHT x Q2 = 0) :
        correctedObservable F δTM δHT x Q2 = F x Q2

        Zero-correction recovery theorem to baseline observable.

        source
        structure EpsilonEridani.QFT.Scattering.DIS.Corrections.BoundedCorrections (δTM : TargetMassCorrection) (δHT : HigherTwistCorrection) :
        Prop

        Bounded-corrections assumption bundle for stability interfaces.

        • tmBound (x Q2 : ℝ) : |δTM x Q2| ≤ 1
        • htBound (x Q2 : ℝ) : |δHT x Q2| ≤ 1
        Instances For
          source
          theorem EpsilonEridani.QFT.Scattering.DIS.Corrections.correctedObservable_sub_baseline_abs_le (F : ℝ → ℝ → ℝ) (δTM : TargetMassCorrection) (δHT : HigherTwistCorrection) (h : BoundedCorrections δTM δHT) (x Q2 : ℝ) :
          |correctedObservable F δTM δHT x Q2 - F x Q2| ≤ 2

          The stability statement the bounded-corrections bundle exists to support: a corrected observable stays within 2 of its baseline, uniformly in x and Q².