Expert review
Start from a task, inspect its mathematical proof, then locate the real library result. Each core is listed once under its first library; all additional domain memberships remain visible in its task and curriculum.
Machine-readable graph anchors and coverage boundaries · Audited structural graph tasks
An anchor is a location, not a proof edge. Imports, compiled proof-body occurrences and conceptual parallels have different meanings. Existing Lean support does not certify an entire natural-language answer.
Log-Concave Sampling · 4 task cores
- A quadratic envelope from one midpoint
centered_quadratic_lower_bound_of_strongConvexOn_minimizer· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- A log-concave shape is not yet a probability density
logConcaveOn_exp_neg_of_convexOn· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- From Gibbs Poincaré to a directional covariance bound
gibbs_linear_covariance_upper· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- From the Boolean cube to compact Gaussian log-Sobolev
compact_gaussian_logSobolev· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
SampleWiki research problems · 4 task cores
- Adaptive hybrid error does not certify expected cost
abs_real_comp_commonSuffix_sub_le_integral_eventBound· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- What kind of guarantee does a sampling claim describe?
abs_real_comp_sub_le· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Averaging a conditional event-error bound
abs_real_comp_sub_le_integral_eventBound· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- Can the SPHMC smoothing argument survive weak convexity?
gibbs_linear_covariance_upper· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
Optimisation · 6 task cores
- PL descent: the sign of the contraction factor
gradient_descent_pl_value_bound· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- Reading a PL inequality before using an algorithm
gradient_descent_pl_value_bound· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Why a global Lipschitz function bounds its supporting vectors
norm_le_of_supportsAt· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- From subgradient energy to a finite-run best iterate
exists_gap_le· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- An actual gradient flow: objective decay with the zero-curvature branch
value_le· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- Chewi Optimization Exercise 3.2: the balanced gradient step
optimal_gradient_step· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
Riemannian Optimisation · 4 task cores
- Why a sphere gradient is a projected ambient gradient
quadratic_feature_potential_tangent_gradient· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Which space contains the sphere gradient?
quadratic_feature_potential_tangent_gradient· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- A quadratic gradient through the actual sphere differential
sphere_rayleigh_characterization· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- From a selected-curve chord inequality to its first-order bound
firstOrder_geodesicConvexity· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
Statistical Optimal Transport · 4 task cores
- Wasserstein symmetry without an optimal plan
wassersteinDistance_comm· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- What information does a coupling contain?
isCoupling_prod· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Recovering joint probability mass from one marginal
isProbabilityMeasure_of_isCoupling_left· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- Gluing the right joint law before applying Minkowski
wassersteinDistance_lt_add_of_lt· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
Discrete Sampling · 3 task cores
- Null atoms in a random-scan balance proof
randomScan_isReversible· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- One random-site step is not one sweep
randomScan· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Tensorizing a two-point entropy bound without losing the flip constant
bernoulli_function_logSobolev· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
Markov Chain Monte Carlo · 4 task cores
- From atomic balance to reversibility
isReversible_of_singleton_balance· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- Invariant, reversible and convergent are different claims
isReversible_of_singleton_balance· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.
- Why retaining one coordinate and conditionally resampling the other is invariant
heatBathSnd_invariant· Graph position · Exact sourceAligned Lean task; explanatory scope is separate.
- One null set for every event, or a different null set for each event?
abs_real_comp_sub_le_integral_eventBound· Graph position · Exact sourceFormal support, not an aligned fixed Lean task.