Documentation
LeanPool
.
ParameterFreeGradient
.
Imports
Search
return to top
source
Imports
Init
LeanPool.ParameterFreeGradient
LeanPool.ParameterFreeGradient.Solution
LeanPool.ParameterFreeGradient.V7
LeanPool.ParameterFreeGradient.O3.AboveTwo
LeanPool.ParameterFreeGradient.O3.Anchor
LeanPool.ParameterFreeGradient.O3.BelowTwo
LeanPool.ParameterFreeGradient.O3.Controller
LeanPool.ParameterFreeGradient.O3.Euclidean
LeanPool.ParameterFreeGradient.O3.Foundation
LeanPool.ParameterFreeGradient.O3.Geometry
LeanPool.ParameterFreeGradient.O3.GeometryExperimental
LeanPool.ParameterFreeGradient.O3.Oracle
LeanPool.ParameterFreeGradient.O3.Stage10EuclideanGuards
LeanPool.ParameterFreeGradient.O3.Stage11Amortization
LeanPool.ParameterFreeGradient.O3.Stage11RConditionBar
LeanPool.ParameterFreeGradient.O3.Stage12AAnchorMachine
LeanPool.ParameterFreeGradient.O3.Stage2BelowGeometry
LeanPool.ParameterFreeGradient.O3.Stage2RouteA
LeanPool.ParameterFreeGradient.O3.Stage2RouteB
LeanPool.ParameterFreeGradient.O3.Stage2RouteC
LeanPool.ParameterFreeGradient.O3.Stage2RouteD
LeanPool.ParameterFreeGradient.O3.Stage3Anchor
LeanPool.ParameterFreeGradient.O3.Stage3AnchorNorming
LeanPool.ParameterFreeGradient.O3.Stage3Descent
LeanPool.ParameterFreeGradient.O3.Stage4AlgebraRadius
LeanPool.ParameterFreeGradient.O3.Stage8EuclideanGap
LeanPool.ParameterFreeGradient.O3.Stage8EuclideanMinimizer
LeanPool.ParameterFreeGradient.O3.Stage8EuclideanPhase
LeanPool.ParameterFreeGradient.O3.Stage8EuclideanRadius
LeanPool.ParameterFreeGradient.O3.Stage8EuclideanWeights
LeanPool.ParameterFreeGradient.O3.Stage9Certificate
LeanPool.ParameterFreeGradient.O3.Stage9Execution
LeanPool.ParameterFreeGradient.O3.Stage9FiniteDataOGMG
LeanPool.ParameterFreeGradient.O3.Stage9Pairing
LeanPool.ParameterFreeGradient.O3.Stage9Telescoping
LeanPool.ParameterFreeGradient.O3.Stage9Theta
LeanPool.ParameterFreeGradient.V7.AboveTwoStatements
LeanPool.ParameterFreeGradient.V7.BelowTwoStatements
LeanPool.ParameterFreeGradient.V7.ControllerStatements
LeanPool.ParameterFreeGradient.V7.EuclideanStatements
LeanPool.ParameterFreeGradient.V7.FiniteProgram
LeanPool.ParameterFreeGradient.V7.Foundation
LeanPool.ParameterFreeGradient.V7.Guards
LeanPool.ParameterFreeGradient.V7.LowerBoundStatements
LeanPool.ParameterFreeGradient.V7.MainStatement
LeanPool.ParameterFreeGradient.V7.PositiveModel
LeanPool.ParameterFreeGradient.V7.StrictModel
LeanPool.ParameterFreeGradient.V7.StrictStatements
LeanPool.ParameterFreeGradient.V7.TrialInterfaces
LeanPool.ParameterFreeGradient.V7.Proofs.Anchor
LeanPool.ParameterFreeGradient.V7.Proofs.Euclidean
LeanPool.ParameterFreeGradient.V7.Proofs.GuardAdapters
LeanPool.ParameterFreeGradient.V7.Proofs.ResidualAlgebra
LeanPool.ParameterFreeGradient.V7.Proofs.Shared
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1AxiomAudit
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.AnalyticBridge
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Certificate
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Correctness
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Ledger
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Machine
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Proof
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Refinement
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Semantics
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Shapes
LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.SourceData
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2.Controller
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2.Geometric
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2.GuardSoundness
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2.PathShape
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2Resume.Amortization
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2Resume.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2Resume.Positivity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage2Resume.Transport
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwo.Dual
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwo.Geometry
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwo.Identity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwo.Primal
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoResumeS3E.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoResumeS3E.GuardScaling
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.AnalyticBridge
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Bounds
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Certificate
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Coefficients
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Contract
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.DualRecursion
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.DualTrajectory
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Ledger
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Machine
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Normalization
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.PrimalTrajectory
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Proof
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Semantics
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Shapes
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.Constants
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.Geometry
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.Identity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.PartialClosure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.PrimalResidual
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwo.WeightBalance
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoDualPhase.AnalyticPrefix
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoDualPhase.DualEnergy
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoDualPhase.PhaseBounds
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.AnalyticBridge
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Bounds
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Certificate
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Coefficients
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Contract
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Ledger
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Machine
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Proof
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Semantics
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Shapes
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.Trajectory
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoFinalTrial.TrajectoryDefinitions
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoPrimalRepair.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage4AboveTwoPrimalRepair.PrimalEnergy
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLower.KernelElementary
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLower.LocalityBridge
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLower.Parameters
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerResume.InfimalAttainment
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerResume.InfimalLocalityClosure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.BaseGradient
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.ConditionalSmoothness
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.Construction
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.DimensionControl
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.EnvelopeDerivative
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.EnvelopeSupport
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.ExactPairCompletion
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.KernelAssembly
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.KernelCocoercivity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.KernelConvexity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.KernelHessianStructure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.OptimizerRadius
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.OutsideGradient
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.PhysicalLower
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.PrimalOptimality
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.QueryGap
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.SymmetryClassification
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.SymmetryEquivariance
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5A2Envelope.SymmetryLinearization
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AFinalRepair.OriginFrechet
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AGlobalC2.Calculus
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AGlobalC2.Continuity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AGlobalC2.Core
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AGlobalC2.QuadraticBound
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AHessianContinuity.HessianContinuity
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5ARepair.InfimalLocality
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5ARepair.KernelAmbientHessian
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5ARepair.KernelAmbientNonzero
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5ARepair.KernelLineCalculus
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5ARepair.Parameters
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.CompletedTrace
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.CompletionData
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.LocalTrialAdapter
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.LowerTheorem
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.ObjectiveData
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.Optimality
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.PhysicalAnalytic
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.PhysicalScaling
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.PrefixState
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.PrefixSync
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.RateAlgebra
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.UnitInstance
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.UpperAnalytic
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.UpperTheorem
LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5F.UpperTrial
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.AffineTrace
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.HSelection
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.HardInstance
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.Indistinguishability
LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.ScalarHard
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.Displacement
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.Expected
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.MeasurableTrace
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.Randomized
LeanPool.ParameterFreeGradient.V7.Proofs.Stage7StrictRandomizedExpected.Transfer
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Accounting
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.AnchorSplice
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.AxiomAudit
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Closure
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Controller
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.History
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.LocalDispatch
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.LocalSpec
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Main
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.MainExecution
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Refinement
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.RuntimeMachine
LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.WholePaperAudit
Imported by