Project-declaredLean 4.8.0
Snap dist
snap_dist
Plain-language statement
Snap produces a close oracle
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Source-pinned research
Research proof index
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
View proof record
Project-declaredLean 4.8.0
Snaps prob
snaps_prob
Plain-language statement
Snapping doesn't changed prob for close p
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Soundness p
soundness_p
Plain-language statement
Soundness for any valid parameters
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Soundness
soundness'
Plain-language statement
Bob wins the debate with probability ≥ 8/15
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.32.0
Basis eq mfderiv model Diffeo single
Space.basis_eq_mfderiv_modelDiffeo_single
Plain-language statement
The derivative of modelDiffeo provides an equivalence between Space d and EuclideanSpace ℝ (Fin d). This equivalences takes the basis of EuclideanSpace ℝ (Fin d) to the basis of Space d, and vice versa.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Constant Time dist Space Deriv
Space.constantTime_distSpaceDeriv
Project documentation
Distributions on Time × Space d from distributions on Space d. These distributions are constant in time. -/ def constantTime {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} : ((Space d) →d[ℝ] M) →ₗ[ℝ] (Time × Space d) →d[ℝ] M where toFun f := f ∘L timeIntegralSchwartz map_add' f g := by ext η simp map_smul' c f := by ext η simp lemma const...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.