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 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 913 to 918 of 2,569 results.
E₂E₄_sub_E₆_div_q_tendsto
Mathematical statement
(E₂E₄ - E₆) / q → 720 as im(z) → ∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₄_eq_H_sum_sq
Mathematical statement
E₄.toFun = H₂² + H₂H₄ + H₄². Both are weight-4 level-1 modular forms tending to 1 at ∞, so their difference is a weight-4 cusp form, hence zero.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₄_sigma_qexp
Mathematical statement
E₄ as explicit tsum (from E4_q_exp PowerSeries coefficients). Uses hasSum_qExpansion to convert from PowerSeries to tsum form.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
eagerRandomOracle_evalDist_generateSeed_bind
Mathematical statement
The eager random oracle, averaged over a uniformly sampled seed, matches the fresh independent-query semantics of evalDist. This is because the pre-sampled seed values are i.i.d. uniform, exactly matching fresh oracle queries. This is the analog of seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run' but for eagerRandomOracle (which falls...
Source project: VCVio
Person-level attribution pending.
Electromagnetism.DistElectromagneticPotential.distTensorDeriv_basis_repr_apply
Project documentation
The creation of an electromagnetic potential from a static vector potential. -/ noncomputable def ofStaticVectorPotential {d} (c : SpeedOfLight) : ((Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) →ₗ[ℝ] DistElectromagneticPotential d := ofVectorPotential c ∘ₗ Space.constantTime TODO "Add a constructor for DistElectromagneticPotential from electric and magnetic f...
Source project: Physlib
Person-level attribution pending.
Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor
Project documentation
The variational gradient of the free current potential for distributional potentials. -/ noncomputable def gradFreeCurrentPotential {d} : DistLorentzCurrentDensity d →ₗ[ℝ] ((SpaceTime d) →d[ℝ] Lorentz.Vector d) where toFun J := { toFun ε := ∑ μ, (η μ μ • (J ε μ) • Lorentz.Vector.basis μ) map_add' ε₁ ε₂ := by simp [Finset.sum_add_distrib, add_smul] map_smu...
Source project: Physlib
Person-level attribution pending.