therefore
Sign up
Open navigation

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 4 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

4 results

Clear filters
Project-declaredLean 4.32.0

Dist Grad eq sum basis

Space.distGrad_eq_sum_basis

Project documentation

The gradient of a distribution (Space d) →d[ℝ] ℝ as a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)). -/ noncomputable def distGrad {d} : ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) where toFun f := basis.repr.toContinuousLinearMap ∘L ((InnerProductSpace.toDual ℝ (Space d)).symm.toContinuousLinearMap).comp (fderivD ℝ...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Dist Grad to Fun eq dist Deriv

Space.distGrad_toFun_eq_distDeriv

Project documentation

The gradient of a distribution (Space d) →d[ℝ] ℝ as a distribution (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)). -/ noncomputable def distGrad {d} : ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] (Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d)) where toFun f := basis.repr.toContinuousLinearMap ∘L ((InnerProductSpace.toDual ℝ (Space d)).symm.toContinuousLinearMap).comp (fderivD ℝ...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Grad inner space unit vector

Space.grad_inner_space_unit_vector

Plain-language statement

The gradient in the direction of the space position.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Integrable is Dist Bounded inner grad schwartz Map

Space.integrable_isDistBounded_inner_grad_schwartzMap

Project documentation

The gradient of the inner product is given by 2 • x. -/ lemma grad_inner {d : ℕ} : ∇ (fun y : Space d => ⟪y, y⟫_ℝ) = fun z => (2 : ℝ) • basis.repr z := by ext z i rw [grad_apply, deriv_eq_inner_self] simp lemma grad_inner_left {d : ℕ} (x : Space d) : ∇ (fun y : Space d => ⟪y, x⟫_ℝ) = fun _ => basis.repr x := by ext z i simp [Space.grad] lemma grad_inner...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record