Swap xx heat Kernel
swap_xx_heatKernel
Plain-language statement
Swap the second spatial derivative with the integral .
Source project: PDE
Person-level attribution pending.
Source-pinned research
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
swap_xx_heatKernel
Plain-language statement
Swap the second spatial derivative with the integral .
Source project: PDE
Person-level attribution pending.
SymmEncAlg.cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey
Project documentation
Core uniformity lemma: uniform keygen plus unique key per (message, ciphertext) pair implies every (message, ciphertext) conditional has probability (card K)⁻¹. Both Shannon theorems follow from this.
Source project: VCVio
Person-level attribution pending.
SymmEncAlg.perfectSecrecyAt_of_uniformKey_of_uniqueKey
Plain-language statement
Constructive Shannon direction: if keygen is uniform and each (message, ciphertext) pair is realized by a unique key in support, then perfect secrecy holds. deterministicEnc asserts encryption is deterministic in distribution (singleton support for each fixed (key, message)).
Source project: VCVio
Person-level attribution pending.
tanh_const_mul_hasTemperateGrowth
Plain-language statement
tanh(κx) has temperate growth
Source project: Physlib
Person-level attribution pending.
tanh_hasTemperateGrowth
Plain-language statement
tanh has temperate growth
Source project: Physlib
Person-level attribution pending.
TateCurve.Blueprint.analytic_weierstrass
Project documentation
The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12. Proof sketch: the hypotheses ensure u ∉ qᶻ, and we may choose z, τ with e z = u, e τ = q, 0 < im z < im τ (so z ∉ Λ_τ). Substitute the four q-expansions into the differential...
Source project: Fermat's Last Theorem
Person-level attribution pending.