Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Shapes

Physical observations, guard schedules, and possible outcomes of the below-two trial.

source
noncomputable def V7.Stage3BelowTwoS3F.horizon (p eps M D : ℝ) :
ℕ

The ceiling of the below-two iteration horizon determined by accuracy and trial estimates.

Equations
Instances For
    source
    noncomputable def V7.Stage3BelowTwoS3F.phaseOneOracle {d : ℕ} (x0 : Point d) (M D : ℝ) (oracle : PairOracle d) :
    PairOracle d

    The phase-one oracle normalized around the initial point.

    Equations
    Instances For
      source
      noncomputable def V7.Stage3BelowTwoS3F.phaseOneState {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) :
      PrimalState d

      The normalized phase-one state at its prescribed accuracy-dependent horizon.

      Equations
      Instances For
        source
        noncomputable def V7.Stage3BelowTwoS3F.phaseOneObs {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) :
        Observation d

        The physical oracle observation corresponding to a normalized primal iterate.

        Equations
        Instances For
          source
          noncomputable def V7.Stage3BelowTwoS3F.phaseTwoCenter {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) :
          Point d

          The physical endpoint of phase one used as the center of phase two.

          Equations
          Instances For
            source
            noncomputable def V7.Stage3BelowTwoS3F.phaseTwoOracle {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) :
            PairOracle d

            The phase-two oracle normalized around the completed primal endpoint.

            Equations
            Instances For
              source
              noncomputable def V7.Stage3BelowTwoS3F.phaseTwoObs {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (k : ℕ) :
              Observation d

              The physical oracle observation corresponding to a normalized dual query.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def V7.Stage3BelowTwoS3F.phaseOneNewTrace {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) :
                List (Observation d)

                The new primal observations after the reused initial query.

                Equations
                Instances For
                  source
                  noncomputable def V7.Stage3BelowTwoS3F.phaseTwoNewTrace {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) :
                  List (Observation d)

                  The new dual observations after the reused phase-one endpoint.

                  Equations
                  Instances For
                    source
                    noncomputable def V7.Stage3BelowTwoS3F.phaseOneChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) :
                    List (ObservableGuardCheck d)

                    The consecutive cocoercivity checks in the completed primal prefix.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def V7.Stage3BelowTwoS3F.phaseTwoChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m : ℕ) :
                      List (ObservableGuardCheck d)

                      The consecutive cocoercivity checks in the completed dual prefix.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def V7.Stage3BelowTwoS3F.allChecks {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) (m₁ m₂ : ℕ) :
                        List (ObservableGuardCheck d)

                        The ordered guard checks from the completed prefixes of both phases.

                        Equations
                        Instances For
                          source
                          inductive V7.Stage3BelowTwoS3F.FullShape {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (oracle : PairOracle d) :
                          TrialReport d → ℕ → ℕ → Prop

                          The possible success, scale-failure, and radius outcomes of a below-two trial report.

                          Instances For