Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
production module

AutoSamplingTheory.TechnicalLemmas.Analysis

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.Analysis.UniformRegularizationAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationOracleAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrderAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationTransferAutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexityAutoSamplingTheory.TechnicalLemmas.Analysis.RestartReductionAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexityAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRatesAutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowLastIterateAutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowStationarityAutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValueAutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowContractionAutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowPLAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullbackAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexGradientGapSharpnessAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentSharpnessAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescentAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStepAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarityAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasicAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPLAutoSamplingTheory.TechnicalLemmas.Analysis.CalculusAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexAEDifferentiableAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradientAutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectationAutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCostAutoSamplingTheory.TechnicalLemmas.Analysis.IntegrabilityAutoSamplingTheory.TechnicalLemmas.Analysis.LeftLebesgueAverageAutoSamplingTheory.TechnicalLemmas.Analysis.PairingCyclicMonotonicityAutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleNeighborhoodAutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhoodAutoSamplingTheory.TechnicalLemmas.Analysis.PermutedQuadraticCostAutoSamplingTheory.TechnicalLemmas.Analysis.PrefixIntegralAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrderAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverseAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalencesAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradientAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContractionAutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue
Imported by
AutoSamplingTheory.TechnicalLemmas
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

This aggregator contains no named declarations.