Module functions

Source

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

app
app2
app3
arrow
aubin_property_criteria_ty: AubinPropertyCriteria : (List Real -> List Real -> Prop) -> Prop Aubin (pseudo-Lipschitz) property: set-valued map has Lipschitz-like continuity.
berge_maximum_theorem_ty: BergeMaximumTheorem : (List Real -> Real) -> (List Real -> List Real -> Prop) -> Prop Berge’s maximum theorem: if f is continuous and C is continuous compact-valued, then V(x) = max_{y∈C(x)} f(x,y) is continuous and the argmax correspondence is USC.
bool_ty
borwein_preiss_principle_ty: BorweinPreissPrinciple : (List Real -> Real) -> Prop Smooth variational principle: perturbation by a smooth gauge function.
borwein_preiss_smooth_ty: BorweinPreissSmooth : (List Real -> Real) -> Prop Borwein-Preiss: for any ε > 0, there exists a smooth perturbation realising a minimiser.
bregman_dynamics_ty: BregmanDynamics : (List Real -> Real) -> (List Real -> Real) -> Prop Bregman proximal dynamics: xₖ₊₁ = argmin {f(x) + Dφ(x, xₖ)/λ}.
build_env: Build an Environment with variational analysis kernel axioms.
build_variational_analysis_env: Build an Environment containing variational analysis axioms and theorems.
build_variational_analysis_env_extended: Build the extended variational analysis environment (adds §7 axioms to existing §1-§6).
bundle_method_ty: BundleMethod : (List Real -> Real) -> Prop Bundle method: collects subgradient information in a “bundle” to build cutting planes.
bvar
cerami_condition_ty: Cerami condition : (List Real -> Real) -> Prop Cerami variant of (PS): (1 + ‖x_n‖)‖∇f(x_n)‖ → 0.
check_gamma_convergence_indicator: Check whether a sequence of penalty functions Gamma-converges to the indicator of [a,b]. Only verifies the liminf inequality at a test point.
check_regular_subgradient: Check whether a vector is a regular (Fréchet) subgradient: liminf_{y→x} (f(y) - f(x) - ⟨v, y-x⟩) / ‖y-x‖ ≥ -tol by sampling random directions.
clarke_directional_derivative_ty: ClarkeGeneralisedDirectionalDerivative : (List Real -> Real) -> List Real -> List Real -> Real f°(x;v) = limsup_{y→x, t↓0} (f(y+tv) - f(y))/t.
clarke_generalised_jacobian_ty: ClarkeGeneralisedJacobian : (List Real -> List Real) -> List Real -> Type ∂^C F(x) = conv{lim ∇F(xₙ) | xₙ → x, xₙ ∉ Ω_F}: Clarke generalised Jacobian.
clarke_generalized_gradient_ty: ClarkeGeneralizedGradient : (List Real -> Real) -> List Real -> List Real A selection from Clarke subdifferential (not unique in general).
clarke_gradient_approx: Compute a Clarke-type subgradient via smoothing (convolution with Gaussian). For locally Lipschitz f, approximate Clarke gradient by averaging finite differences.
clarke_stationary_condition_ty: ClarkeStationaryCondition : (List Real -> Real) -> List Real -> Prop 0 ∈ ∂^C f(x): Clarke stationarity as a necessary optimality condition.
clarke_subdiff_chain_rule_ty: ClarkeSubdiffChainRule : Prop Clarke’s chain rule for composite locally Lipschitz functions.
clarke_subdiff_sum_rule_ty: ClarkeSubdiffSumRule : Prop Clarke’s sum rule: ∂^C(f+g)(x) ⊆ ∂^C f(x) + ∂^C g(x).
clarke_subdifferential_ty: ClarkeSubdifferential : (List Real -> Real) -> List Real -> (List Real -> Prop) ∂^C f(x) = conv(∂_L f(x)): convex hull of limiting subdifferential.
cst
deformation_lemma_ty: DeformationLemma : (List Real -> Real) -> Prop Deformation retract of sub-level sets avoiding critical levels.
density_of_minimisers_ty: DensityOfMinimisers : (List Real -> Real) -> Prop The set of strict minimisers is dense (consequence of variational principles).
deville_godefroy_zizler_ty: Deville_Godefroy_Zizler : Prop Deville-Godefroy-Zizler variational principle: smooth bump function perturbation.
douglas_rachford_splitting_ty: DouglasRachfordSplitting : (List Real -> Real) -> (List Real -> Real) -> Prop Douglas-Rachford splitting for minimising f + g via proximal operators.
ekeland_approximate_minimiser: Approximate Ekeland minimiser: finds x_ε near x₀ such that f(x_ε) ≤ f(x₀) and f(x_ε) ≤ f(x) + eps * ‖x - x_ε‖ for all tested x.
ekeland_variational_principle_ty: EkelandVariationalPrinciple : (List Real -> Real) -> Prop For every ε > 0 and near-minimiser x₀ of lsc proper f bounded below, ∃ xε: f(xε) ≤ f(x₀) and f(xε) ≤ f(x) + ε‖x-xε‖ for all x.
ekeland_with_error_bound_ty: EkelandWithErrorBound : (List Real -> Real) -> Real -> Prop Ekeland’s principle with explicit error bound for approximate minimisers.
epi_conv_implies_min_ty: EpiConvergenceImpliesMinConvergence : Prop If f_n epi-converges to f then inf f_n → inf f and argmin_n converges.
epi_convergence_stability_ty: EpiConvergenceStability : Prop Epi-convergence is stable under continuous perturbations of the functionals.
epi_converges_ty: EpiConverges : (Nat -> List Real -> Real) -> (List Real -> Real) -> Prop f_n epi-converges to f: epi(f_n) → epi(f) in the set convergence sense.
epi_liminf_ty: EpiLimInf : (Nat -> List Real -> Real) -> List Real -> Real (e-liminf f_n)(x) = liminf_{y_n → x} liminf_n f_n(y_n).
epi_limsup_ty: EpiLimSup : (Nat -> List Real -> Real) -> List Real -> Real (e-limsup f_n)(x) = liminf_{y_n → x} limsup_n f_n(y_n).
flowering_principle_ty: FloweringPrinciple : Prop Stegall’s “flowering” variational principle in Asplund spaces.
fn_ty
frechet_normal_cone_ty: FrechetNormalCone : (List Real -> Prop) -> List Real -> (List Real -> Prop) N̂(C;x): Fréchet (regular) normal cone — subdifferential of indicator function.
fuzzy_sum_rule_ty: FuzzySum : Prop Fuzzy (approximate) sum rule for regular subdifferentials.
gamma_compactness_ty: GammaCompactness : Prop Every sequence of equi-coercive functions has a Γ-convergent subsequence.
gamma_conv_minimisers_ty: GammaConvergenceMinimisers : Prop Γ-convergence ensures convergence of minimisers and minimum values.
gamma_conv_stability_ty: GammaConvergenceStability : Prop Γ-convergence is stable under addition of continuous perturbations.
gamma_converges_ty: GammaConverges : (Nat -> List Real -> Real) -> (List Real -> Real) -> Prop f_n Γ-converges to f iff Γ-liminf = Γ-limsup = f.
gamma_liminf_ty: GammaLimInf : (Nat -> List Real -> Real) -> List Real -> Real Γ-liminf_n f_n(x) = sup_{U∋x} liminf_n inf_{y∈U} f_n(y).
gamma_limsup_ty: GammaLimSup : (Nat -> List Real -> Real) -> List Real -> Real Γ-limsup_n f_n(x) = sup_{U∋x} lim_n inf_{y∈U} f_n(y).
gradient_flow_ty: GradientFlow : (List Real -> Real) -> Prop Gradient flow: ẋ ∈ -∂f(x), the steepest descent curve in the sense of maximal slope.
hausdorff_continuity_ty: HausdorffContinuity : (List Real -> List Real -> Prop) -> Prop A set-valued map is Hausdorff continuous if d_H(F(x), F(y)) → 0 as y → x.
is_palais_smale_sequence: Check whether a finite sequence is a Palais-Smale sequence: |f(x_n)| bounded AND ‖∇f(x_n)‖ → 0.
is_prox_regular_function_ty: IsProxRegularFunction : (List Real -> Real) -> Real -> Prop f is r-prox-regular: its epigraph is r-prox-regular as a set.
is_prox_regular_set_ty: IsProxRegularSet : (List Real -> Prop) -> Real -> Prop C is r-prox-regular: the projection onto C is single-valued on a tube of radius r.
is_pseudoconvex_ty: IsPseudoconvex : (List Real -> Real) -> Prop f is pseudoconvex: ⟨∇f(x), y-x⟩ ≥ 0 ⟹ f(y) ≥ f(x).
is_quasiconvex_ty: IsQuasiconvex : (List Real -> Real) -> Prop f is quasiconvex: level sets {x | f(x) ≤ α} are convex for all α.
kkt_conditions_ty: KKTConditions : (List Real -> Real) -> (List (List Real -> Real)) -> List Real -> Prop Karush-Kuhn-Tucker necessary optimality conditions.
kuratowski_ryll_nardzewski_ty: KuratowskiRyllNardzewski : (List Real -> List Real -> Prop) -> Prop Kuratowski-Ryll-Nardzewski measurable selection theorem.
licq_ty: LICQ : (List (List Real -> Real)) -> List Real -> Prop Linear Independence CQ: gradients of active constraints are linearly independent.
limiting_normal_cone_ty: LimitingNormalCone : (List Real -> Prop) -> List Real -> (List Real -> Prop) N_L(C; x) = Limsup_{y→x, y∈C} N̂(C; y).
limiting_subdifferential_ty: LimitingSubdifferential : (List Real -> Real) -> List Real -> (List Real -> Prop) Mordukhovich (basic) subdifferential: cluster points of regular subgradients along sequences.
linear_regularity_ty: LinearRegularity : (List (List Real -> Prop)) -> Prop A collection of sets is linearly regular: d(x, ∩Cᵢ) ≤ κ max d(x, Cᵢ).
linking_theorem_ty: LinkingTheorem : (List Real -> Real) -> Prop Abstract linking theorem yielding critical points.
lipschitz_stability_ty: LipschitzStability : (List Real -> List Real) -> Real -> Prop A map F is Lipschitz-stable (calm) with constant κ near a point.
list_ty
lower_dini_derivative_ty: LowerDiniDerivative : (List Real -> Real) -> List Real -> List Real -> Real D₋f(x;v) = liminf_{t↓0} (f(x+tv) - f(x))/t.
metric_regularity_ty: MetricRegularity : (List Real -> List Real -> Prop) -> Real -> Prop F is metrically regular at (x,y) with constant κ: d(x, F⁻¹(y)) ≤ κ d(y, F(x)).
mfcq_ty: MFCQ : (List (List Real -> Real)) -> (List (List Real -> Real)) -> List Real -> Prop Mangasarian-Fromovitz CQ: active constraint gradients + inequality multipliers positively independent.
michael_selection_theorem_ty: MichaelSelectionTheorem : (List Real -> List Real -> Prop) -> Prop Michael’s selection theorem: an LSC map with convex closed values has a continuous selection.
mirror_descent_algorithm_ty: MirrorDescentAlgorithm : (List Real -> Real) -> (List Real -> Real) -> Prop Mirror descent: generalises gradient descent to curved geometries via Bregman divergence.
mordukhovich_coderivative_ty: MordukhovichCoderivative : (List Real -> List Real) -> List Real -> (List Real -> List Real -> Prop) D*F(x)(v): coderivative of a set-valued map F at (x, y).
mordukhovich_criterion_ty: MordukhovichCriterion : (List Real -> Prop) -> List Real -> Prop Mordukhovich normal cone regularity criterion for closed sets.
mordukhovich_subdiff_chain_rule_ty: MordukhovichSubdiffChainRule : Prop Mordukhovich chain rule for compositions of Lipschitz mappings.
mordukhovich_subdiff_sum_rule_ty: MordukhovichSubdiffSumRule : Prop Mordukhovich sum rule with SNC (sequential normal compactness) condition.
morse_index_ty: MorseIndex : (List Real -> Real) -> List Real -> Nat Index of a nondegenerate critical point (dimension of negative eigenspace of Hessian).
morse_inequalities_ty: MorseInequalities : (List Real -> Real) -> Prop Morse inequalities relating critical points and Betti numbers.
mosco_convergence_reflexive_banach_ty: MoscoConvergenceReflexiveBanach : Prop In reflexive Banach spaces, Mosco convergence is equivalent to weak epi + strong epi convergence.
mosco_converges_ty: MoscoConverges : (Nat -> List Real -> Real) -> (List Real -> Real) -> Prop Mosco convergence: combines strong epi and weak epi convergence conditions.
mosco_implies_epi_ty: MoscoImpliesEpi : Prop Mosco convergence implies epi-convergence (in reflexive Banach spaces).
mountain_pass_theorem_ty: MountainPassTheorem : (List Real -> Real) -> Prop If f satisfies (PS) and has a mountain-pass geometry, ∃ critical point.
nat_ty
normal_cone_calculus_ty: NormalConeCalculus : (List Real -> Prop) -> (List Real -> Prop) -> Prop Normal cone calculus: N(C₁ ∩ C₂; x) ⊆ N(C₁; x) + N(C₂; x) under regularity.
normal_cone_inclusion_ty: NormalConeInclusion : Prop Proximal ⊆ Fréchet ⊆ Limiting normal cone (fundamental inclusions).
palais_smale_condition_ty: PalaisSmaleCondition : (List Real -> Real) -> Prop (PS): every sequence with bounded values and gradient → 0 has a convergent subsequence.
penalty_indicator_1d: Compute penalty approximation of indicator function of [a, b]: f_n(x) = n * (max(0, x - b) + max(0, a - x)).
pi
prop
prox_regular_minimisation_ty: ProxRegularMinimisation : (List Real -> Real) -> Real -> Prop Prox-regularity ensures the proximal point algorithm converges at linear rate.
prox_regularity_projection_ty: ProxRegularityProjection : (List Real -> Prop) -> Real -> Prop For r-prox-regular C, proj_C is single-valued on the open r-tube around C.
proximal_normal_cone_ty: ProximalNormalCone : (List Real -> Prop) -> List Real -> (List Real -> Prop) N̂^P(C;x): proximal normals via squared distance to C.
proximal_point_algorithm_ty: ProximalPointAlgorithm : (List Real -> Real) -> Prop Proximal point algorithm: x_{k+1} = prox_{λf}(xₖ) converges to a minimiser.
quasiconvex_level_sets_ty: QuasiconvexLevelSets : (List Real -> Real) -> Real -> Prop Level set {x | f(x) ≤ α} is convex for each α ∈ ℝ when f is quasiconvex.
quasidifferential_ty: Quasidifferential : (List Real -> Real) -> List Real -> Type Quasidifferential ∂f(x) = (Df(x), -Df(x)): pair of convex compact sets characterising df.
real_ty
regular_subdifferential_ty: RegularSubdifferential : (List Real -> Real) -> List Real -> (List Real -> Prop) F-subdifferential (Fréchet): v ∈ D̂f(x) iff liminf_{y→x} (f(y)-f(x)-⟨v,y-x⟩)/‖y-x‖ ≥ 0.
robinson_stability_ty: RobinsonStability : (List Real -> List Real -> Prop) -> Prop Robinson’s stability theorem: MFCQ implies Lipschitz stability of solution maps.
saddle_point_dynamics_ty: SaddlePointDynamics : (List Real -> List Real -> Real) -> Prop Primal-dual saddle point dynamics: (ẋ, ẏ) = (-∂_x L(x,y), ∂_y L(x,y)).
saddle_point_theorem_ty: SaddlePointTheorem : (List Real -> Real) -> Prop Generalisation of mountain pass to saddle geometries.
second_order_necessary_conditions_ty: SecondOrderNecessaryConditions : (List Real -> Real) -> List Real -> Prop SONC: Hessian of Lagrangian is PSD on the critical cone at a local minimiser.
second_order_sufficient_conditions_ty: SecondOrderSufficientConditions : (List Real -> Real) -> List Real -> Prop SOSC: positive definiteness of Lagrangian Hessian on the critical cone.
seq_ty
star_shaped_minimisation_ty: StarShapedMinimisation : Prop Variational principle for star-shaped constraint sets.
strict_differentiability_ty: StrictDifferentiability : (List Real -> List Real) -> List Real -> Prop F is strictly differentiable at x: limit of (F(y)-F(z))/(y-z) as y,z→x is uniform.
strict_quasiconvexity_ty: StrictQuasiconvexity : (List Real -> Real) -> Prop Strict quasiconvexity: f(λx + (1-λ)y) < max(f(x), f(y)) for x≠y, λ∈(0,1).
subdiff_chain_rule_ty: SubdiffChainRule : Prop Chain rule for limiting subdifferential of composed mappings.
subdiff_sum_rule_ty: SubdiffSumRule : Prop Limiting subdiff of sum: ∂(f+g)(x) ⊆ ∂f(x) + ∂g(x) under SNEC condition.
subsmooth_function_ty: SubsmoothFunction : (List Real -> Real) -> Prop A subsmooth function: regular subdifferential equals limiting subdifferential everywhere.
topological_epi_convergence_ty: TopologicalEpiConvergence : (Nat -> List Real -> Real) -> (List Real -> Real) -> Prop Epi-convergence in a general topological space setting.
trust_region_principle_ty: TrustRegionPrinciple : Prop Trust-region model for approximate variational principles.
type0
uniformly_prox_regular_ty: UniformlyProxRegular : (List Real -> Prop) -> Real -> Prop Uniformly r-prox-regular: same r works at every boundary point.
upper_dini_derivative_ty: UpperDiniDerivative : (List Real -> Real) -> List Real -> List Real -> Real D⁺f(x;v) = limsup_{t↓0} (f(x+tv) - f(x))/t.
vec_ty

Module functions

Module functions Copy item path

Functions§

Module functions