Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Machine

Finite causal query programs implementing the above-two primal and dual phases.

source
@[instance_reducible]
noncomputable def V7.Stage4AboveTwoFinalTrial.machinePropDecidable (q : Prop) :
Decidable q

Classical proposition decisions used locally by the above-two trial machine.

Equations
Instances For
    source
    noncomputable def V7.Stage4AboveTwoFinalTrial.dualProgram {d : ℕ} (p eps M D eta : ℝ) (n k : ℕ) (center q r : Point d) (G : VectorSeq d) (previous : Observation d) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) :
    CausalProgram.Program d fuel

    The above-two dual query program with early accuracy or guard-failure termination.

    Equations
    Instances For
      source
      def V7.Stage4AboveTwoFinalTrial.phaseOneBudget (nD : ℕ) :
      ℕ → ℕ

      The remaining primal query budget plus the prescribed dual horizon.

      Equations
      Instances For
        source
        noncomputable def V7.Stage4AboveTwoFinalTrial.phaseOneProgram {d : ℕ} (p eps M D eta₁ eta₂ : ℝ) (x0 : Point d) (n₁ n₂ k : ℕ) (state : PrimalState d) (previous : Observation d) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) :
        CausalProgram.Program d (phaseOneBudget n₂ fuel)

        The above-two primal query program that initializes the dual phase at its endpoint.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def V7.Stage4AboveTwoFinalTrial.aboveLocalTrial {d : ℕ} (p eps : ℝ) (x0 : Point d) (nf nd : ℕ) :
          LocalTrial d

          The complete above-two local trial with its primal and dual horizons.

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