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
Space.integrableOn_norm_rpow_iff_of_isBounded_nhds
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on a bounded neighborhood of the origin iff 0 < d + p.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_of_isBounded_compl_nhds
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on a bounded subset with the origin in its exterior.
Source project: Physlib
Person-level attribution pending.
Space.integrableOn_norm_rpow_shell
Plain-language statement
The function x ↦ ‖x‖ᵖ is integrable on the shell {x : Space d | 0 < a ≤ ‖x‖ ∧ ‖x‖ < b}.
Source project: Physlib
Person-level attribution pending.
Space.IsDistBounded.add
Project documentation
The boundedness condition on a function Space d → F for it to form a distribution. -/ @[fun_prop] def IsDistBounded {d : ℕ} (f : Space d → F) : Prop := AEStronglyMeasurable (fun x => f x) volume ∧ ∃ n, ∃ c : Fin n → ℝ, ∃ g : Fin n → Space d, ∃ p : Fin n → ℤ, (∀ i, 0 ≤ c i) ∧ (∀ i, - (d - 1 : ℕ) ≤ p i) ∧ ∀ x, ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p i namespace...
Source project: Physlib
Person-level attribution pending.
Space.IsDistBounded.const_smul
Project documentation
The boundedness condition on a function Space d → F for it to form a distribution. -/ @[fun_prop] def IsDistBounded {d : ℕ} (f : Space d → F) : Prop := AEStronglyMeasurable (fun x => f x) volume ∧ ∃ n, ∃ c : Fin n → ℝ, ∃ g : Fin n → Space d, ∃ p : Fin n → ℤ, (∀ i, 0 ≤ c i) ∧ (∀ i, - (d - 1 : ℕ) ≤ p i) ∧ ∀ x, ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p i namespace...
Source project: Physlib
Person-level attribution pending.
Space.IsDistBounded.integrable_mul_inv_pow
Project documentation
The boundedness condition on a function Space d → F for it to form a distribution. -/ @[fun_prop] def IsDistBounded {d : ℕ} (f : Space d → F) : Prop := AEStronglyMeasurable (fun x => f x) volume ∧ ∃ n, ∃ c : Fin n → ℝ, ∃ g : Fin n → Space d, ∃ p : Fin n → ℤ, (∀ i, 0 ≤ c i) ∧ (∀ i, - (d - 1 : ℕ) ≤ p i) ∧ ∀ x, ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p i namespace...
Source project: Physlib
Person-level attribution pending.