Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.GlobalVariance.Defs.Core

Section 8 global variance: core definitions #

Basic question and answer types (axis-parallel line questions, point-pair questions) underlying the Section 8 global-variance construction.

References #

Basic question and answer types #

source
@[reducible, inline]
abbrev MIPStarRE.LDT.GlobalVariance.AxisParallelLineQuestion (params : Parameters) :
Type

An axis-parallel line together with a point queried on that line.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPStarRE.LDT.GlobalVariance.PointPairQuestion (params : Parameters) :
    Type

    A pair of points used for local or global variance comparisons.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MIPStarRE.LDT.GlobalVariance.DegreeBoundedPolynomialAnswer (params : Parameters) [FieldModel params.q] :
      Type u_2

      Degree-bounded polynomial answers: global low-individual-degree polynomials over the chosen field model, i.e. pairs of a multivariate polynomial and a proof that each individual degree is at most params.d. Coerces to a raw function Point params → Fq params via Polynomial.toFun, so downstream callers may still write g u to evaluate.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev MIPStarRE.LDT.GlobalVariance.DegreeBoundedLineAnswer (params : Parameters) [FieldModel params.q] :
        Type u_2

        Degree-bounded axis-line answers: univariate polynomials of degree at most params.d over the chosen field model. Coerces to a raw function Fq params → Fq params via AxisLinePolynomial.toFun.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable instance MIPStarRE.LDT.GlobalVariance.instFintypeAxisParallelLine (params : Parameters) :
          Fintype (AxisParallelLine params)

          Axis-parallel lines are finitely enumerable via their base point and direction.

          Equations
          source
          instance MIPStarRE.LDT.GlobalVariance.instNonemptyPolynomial (params : Parameters) [FieldModel params.q] :
          Nonempty (Polynomial params)

          A default low-degree polynomial witnessing nonemptiness of the finite polynomial answer type.

          source
          def MIPStarRE.LDT.GlobalVariance.pointOnLine {params : Parameters} [FieldModel params.q] (qu : AxisParallelLineQuestion params) :
          Prop

          A valid axis-parallel line question pairs a line with a point lying on it.

          Equations
          Instances For
            source
            def MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionParameter {params : Parameters} [FieldModel params.q] (qu : AxisParallelLineQuestion params) :
            Fq params

            The affine line parameter of the sampled point in an axis-parallel line question.

            For a line ℓ(t) = base + t e_i, the sampled point u has affine parameter u_i - base_i. This is the parameter used by the axis-parallel line-test API; it is not the raw coordinate u_i unless the line base has zero in direction i.

            Equations
            Instances For
              source
              @[simp]
              theorem MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionParameter_pointAt {params : Parameters} [FieldModel params.q] (ℓ : AxisParallelLine params) (t : Fq params) :
              axisParallelLineQuestionParameter (ℓ, ℓ.pointAt t) = t

              The recovered parameter of ℓ.pointAt t is exactly t.

              source
              noncomputable def MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionDistribution (params : Parameters) [FieldModel params.q] :
              Distribution (AxisParallelLineQuestion params)

              The distribution of an axis-parallel line together with a point queried on it.

              The paper samples u ∈ F_q^m uniformly, then samples a direction i uniformly, and finally takes the axis-parallel line through u in direction i. Since AxisParallelLineQuestion params is represented as a pair (ℓ, u), we realize this as the normalized uniform distribution on the finite set of incident pairs, i.e. those with u ∈ ℓ.

              Equations
              Instances For
                source
                theorem MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionDistribution_support_nonempty (params : Parameters) [FieldModel params.q] :
                (axisParallelLineQuestionDistribution params).support.Nonempty

                The incident axis-line sample space is nonempty: take any point, any coordinate direction, and the canonical line through that point.

                source
                theorem MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionDistribution_isProbability (params : Parameters) [FieldModel params.q] :
                (axisParallelLineQuestionDistribution params).IsProbability

                The incident axis-line distribution is a probability distribution.

                source
                theorem MIPStarRE.LDT.GlobalVariance.axisParallelLineQuestionDistribution_toPMF (params : Parameters) [FieldModel params.q] :
                (axisParallelLineQuestionDistribution params).toPMF ⋯ = PMF.uniformOfFinset (axisParallelLineQuestionDistribution params).support ⋯

                The incident axis-line distribution is Mathlib's uniform PMF on its finite incident-pair support.

                source
                noncomputable def MIPStarRE.LDT.GlobalVariance.polynomialDistribution (params : Parameters) [FieldModel params.q] :
                Distribution (Polynomial params)

                The uniform distribution over bundled low-individual-degree polynomials.

                Equations
                Instances For
                  source
                  theorem MIPStarRE.LDT.GlobalVariance.polynomialDistribution_isProbability (params : Parameters) [FieldModel params.q] :
                  (polynomialDistribution params).IsProbability

                  The polynomial-answer distribution is a probability distribution.

                  source
                  theorem MIPStarRE.LDT.GlobalVariance.polynomialDistribution_toPMF (params : Parameters) [FieldModel params.q] :
                  (polynomialDistribution params).toPMF ⋯ = PMF.uniformOfFintype (Polynomial params)

                  The polynomial-answer distribution is Mathlib's uniform PMF on the finite answer type.