Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Tails

Coarse-graining support: Support.Book.Ch04.Tails #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Public Chapter 4 weak-tail notation #

This file re-exports the already-developed independent-sums tail vocabulary under the Book.Ch04 namespace.

source
@[reducible, inline]
abbrev HCPolySupport.Book.Ch04.IsBigOWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : Ω → ℝ) (A : ℝ) :
Prop

The weak-Orlicz upper-tail relation X ≤ O_Psi(A).

Equations
Instances For
    source
    @[reducible, inline]
    abbrev HCPolySupport.Book.Ch04.upperTailEvent {Ω : Type u_1} :
    (Ω → ℝ) → ℝ → Set Ω

    The upper-tail event {X > a} used by the weak-tail notation.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev HCPolySupport.Book.Ch04.absTailEvent {Ω : Type u_1} :
      (Ω → ℝ) → ℝ → Set Ω

      The absolute upper-tail event {|X| > a}.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev HCPolySupport.Book.Ch04.IsBigO {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : Ω → ℝ) (A : ℝ) :
        Prop

        The symmetric weak-Orlicz relation X = O_Psi(A).

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev HCPolySupport.Book.Ch04.AdmissiblePsi (Ψ : ℝ → ℝ) :
          Prop

          Admissible weak-tail functions.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev HCPolySupport.Book.Ch04.HasPsiGrowth (Ψ : ℝ → ℝ) (K : ℝ) :
            Prop

            The Chapter 4 growth hypothesis t Psi(t) ≤ Psi(K t) for t ≥ 1.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev HCPolySupport.Book.Ch04.HasPsiAbstractDoubling (Ψ : ℝ → ℝ) (q C₀ : ℝ) :
              Prop

              The abstract doubling package used in the finite-family weak-tail triangle inequality.

              Equations
              Instances For
                source
                @[reducible, inline]
                noncomputable abbrev HCPolySupport.Book.Ch04.gammaSigma (σ : ℝ) :
                ℝ → ℝ

                The stretched-exponential model class Gamma_sigma.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  noncomputable abbrev HCPolySupport.Book.Ch04.psiSigma (σ : ℝ) :
                  ℝ → ℝ

                  The log-normal model class Psi_sigma.

                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev HCPolySupport.Book.Ch04.HasGammaMomentGrowthWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (σ : ℝ) (X : Ω → ℝ) (M : ℝ) :
                    Prop

                    Witness-level p^(1/sigma) moment growth for the stretched-exponential class.

                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev HCPolySupport.Book.Ch04.HasGammaMomentGrowth {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (σ : ℝ) (X : Ω → ℝ) :
                      Prop

                      Existential p^(1/sigma) moment growth for the stretched-exponential class.

                      Equations
                      Instances For