production module

`AutoSamplingTheory.TechnicalLemmas.Analysis`

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

Imports

Imported by

AutoSamplingTheory.TechnicalLemmas

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Analysis.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk
import AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk
import AutoSamplingTheory.TechnicalLemmas.Analysis.UniformRegularization
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationOracle
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrder
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationTransfer
import AutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexity
import AutoSamplingTheory.TechnicalLemmas.Analysis.RestartReduction
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexity
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowLastIterate
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowStationarity
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValue
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowContraction
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowPL
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence
import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullback
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexGradientGapSharpness
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentSharpness
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL
import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexAEDifferentiable
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
import AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod
import AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectation
import AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCost
import AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability
import AutoSamplingTheory.TechnicalLemmas.Analysis.LeftLebesgueAverage
import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCyclicMonotonicity
import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleNeighborhood
import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhood
import AutoSamplingTheory.TechnicalLemmas.Analysis.PermutedQuadraticCost
import AutoSamplingTheory.TechnicalLemmas.Analysis.PrefixIntegral
import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder
import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexMinimizer
import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverse
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2
import AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries
import AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue
import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature
import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoPositiveWeights
import AutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator
import AutoSamplingTheory.TechnicalLemmas.Analysis.WeakGradientZero
import AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap
import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum

/-!
# Analysis technical lemma arsenal

Parent import surface for reusable analysis lemmas.
-/