IsDistBounded

📁 Source: PhysLean/SpaceAndTime/Space/IsDistBounded.lean

Statistics

Metric	Count
Definitions IsDistBounded	1
Theorems add, aeStronglyMeasurable_fderiv_schwartzMap_smul, aeStronglyMeasurable_inv_pow, aeStronglyMeasurable_schwartzMap_smul, aeStronglyMeasurable_time_schwartzMap_smul, aestronglyMeasurable, comp_add_right, comp_sub_right, component_mul_isDistBounded, component_smul_isDistBounded, congr, const, const_fun_smul, const_mul_fun, const_smul, fun_add, inner_left, instHasTemperateGrowthProdProdOfOpensMeasurableSpace, integrable_mul_inv_pow, integrable_space, integrable_space_fderiv, integrable_space_fderiv_mul, integrable_space_mul, integrable_time_space, integral_mul_schwartzMap_bounded, inv, inv_pow_smul_repr_self, inv_pow_smul_self, inv_shift, isDistBounded_mul_inner, isDistBounded_mul_inner', isDistBounded_mul_inner_of_smul_norm, isDistBounded_smul_inner, isDistBounded_smul_inner_of_smul_norm, isDistBounded_smul_self, isDistBounded_smul_self_repr, log_norm, mono, mul_const_fun, mul_inner_pow_neg_two, nat_pow, nat_pow_shift, neg, norm, norm_add, norm_add_nat_pow, norm_add_pos_nat_zpow, norm_mul_isDistBounded, norm_smul_isDistBounded, norm_smul_nat_pow, norm_smul_zpow, norm_sub, pi_comp, pow, pow_shift, smul_const, sum, sum_fun, vector_component, zero, zpow_smul_repr_self, zpow_smul_repr_self_sub, zpow_smul_self	63
Total	64

Space

Definitions

Name	Category	Theorems
IsDistBounded 📖	MathDef	30 math math: IsDistBounded.inv_shift, IsDistBounded.normPowerSeries_single, IsDistBounded.zpow_smul_self, IsDistBounded.normPowerSeries_deriv, IsDistBounded.nat_pow_shift, IsDistBounded.zpow_smul_repr_self, IsDistBounded.normPowerSeries_zpow, IsDistBounded.norm_smul_nat_pow, IsDistBounded.pow, IsDistBounded.norm_sub, gradient_dist_normPowerSeries_zpow_tendsTo, IsDistBounded.normPowerSeries_log, IsDistBounded.pow_shift, IsDistBounded.zpow_smul_repr_self_sub, IsDistBounded.norm_add_pos_nat_zpow, IsDistBounded.norm_add_nat_pow, IsDistBounded.mul_inner_pow_neg_two, IsDistBounded.log_norm, distGrad_distOfFunction_norm_zpow, IsDistBounded.norm_smul_zpow, IsDistBounded.norm, IsDistBounded.normPowerSeries_fderiv, IsDistBounded.const, IsDistBounded.inv_pow_smul_self, IsDistBounded.inv_pow_smul_repr_self, IsDistBounded.nat_pow, IsDistBounded.inv, IsDistBounded.zero, IsDistBounded.norm_add, IsDistBounded.normPowerSeries_inv

Space.IsDistBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Space.IsDistBounded	Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
aeStronglyMeasurable_fderiv_schwartzMap_smul 📖	mathematical	Space.IsDistBounded	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace Space.instSeminormedAddCommGroup Space.instAddCommGroup Space.instModuleReal	—	Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
aeStronglyMeasurable_inv_pow 📖	mathematical	Space.IsDistBounded	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace Space.instNorm	—	Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
aeStronglyMeasurable_schwartzMap_smul 📖	mathematical	Space.IsDistBounded	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
aeStronglyMeasurable_time_schwartzMap_smul 📖	mathematical	Space.IsDistBounded	Time Space Time.instMeasurableSpace Space.instMeasurableSpace Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instBorelSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace Time.instNormedSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
aestronglyMeasurable 📖	mathematical	Space.IsDistBounded	Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace
comp_add_right 📖	mathematical	Space.IsDistBounded	Space Space.instAdd	—	Space.instFiniteDimensionalReal Space.instBorelSpace
comp_sub_right 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup	—	comp_add_right
component_mul_isDistBounded 📖	mathematical	Space.IsDistBounded	Space.val	—	component_smul_isDistBounded
component_smul_isDistBounded 📖	mathematical	Space.IsDistBounded	Space.val	—	mono norm_smul_isDistBounded Space.instFiniteDimensionalReal Space.instBorelSpace Space.coordCLM_apply Space.coord_apply aestronglyMeasurable Space.abs_eval_le_norm
congr 📖	—	Space.IsDistBounded Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	—	Space.instFiniteDimensionalReal Space.instBorelSpace
const 📖	mathematical	—	Space.IsDistBounded	—	Space.instFiniteDimensionalReal Space.instBorelSpace
const_fun_smul 📖	—	Space.IsDistBounded	—	—	const_smul
const_mul_fun 📖	—	Space.IsDistBounded	—	—	const_smul
const_smul 📖	mathematical	Space.IsDistBounded	Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace
fun_add 📖	—	Space.IsDistBounded	—	—	add
inner_left 📖	—	Space.IsDistBounded	—	—	Space.instFiniteDimensionalReal Space.instBorelSpace
instHasTemperateGrowthProdProdOfOpensMeasurableSpace 📖	—	—	—	—	—
integrable_mul_inv_pow 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Space.instNorm	—	Space.instFiniteDimensionalReal Space.instBorelSpace Space.instSubsingletonOfNatNat Space.instHasTemperateGrowthRadialAngularMeasure Space.integrable_radialAngularMeasure_iff Space.instNontrivialSucc aeStronglyMeasurable_inv_pow
integrable_space 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace Space.instSubsingletonOfNatNat Space.instHasTemperateGrowthRadialAngularMeasure Space.integrable_radialAngularMeasure_iff aestronglyMeasurable
integrable_space_fderiv 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Space.instSeminormedAddCommGroup Space.instAddCommGroup Space.instModuleReal	—	integrable_space
integrable_space_fderiv_mul 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Space.instSeminormedAddCommGroup Space.instAddCommGroup Space.instModuleReal	—	integrable_space
integrable_space_mul 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	integrable_space
integrable_time_space 📖	mathematical	Space.IsDistBounded	Time Space Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Time.instNormedSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace instHasTemperateGrowthProdProdOfOpensMeasurableSpace Space.instHasTemperateGrowthRadialAngularMeasure Space.radialAngularMeasure_zero_eq_volume Space.radialAngularMeasure.eq_1 aeStronglyMeasurable_time_schwartzMap_smul
integral_mul_schwartzMap_bounded 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace integrable_mul_inv_pow aestronglyMeasurable
inv 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	pow
inv_pow_smul_repr_self 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	zpow_smul_repr_self
inv_pow_smul_self 📖	mathematical	—	Space.IsDistBounded Space Space.instNormedAddCommGroup Space.instSMulReal Space.instNorm	—	zpow_smul_self
inv_shift 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup	—	pow_shift
isDistBounded_mul_inner 📖	mathematical	Space.IsDistBounded	Space Space.instInnerReal	—	isDistBounded_smul_inner
isDistBounded_mul_inner' 📖	mathematical	Space.IsDistBounded	Space Space.instInnerReal	—	isDistBounded_smul_inner
isDistBounded_mul_inner_of_smul_norm 📖	mathematical	Space.IsDistBounded Space Space.instNorm Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	Space.instInnerReal	—	Space.instFiniteDimensionalReal Space.instBorelSpace isDistBounded_smul_inner_of_smul_norm
isDistBounded_smul_inner 📖	mathematical	Space.IsDistBounded	Space Space.instInnerReal	—	Space.inner_eq_sum sum_fun const_fun_smul component_smul_isDistBounded
isDistBounded_smul_inner_of_smul_norm 📖	mathematical	Space.IsDistBounded Space Space.instNorm Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	Space.instInnerReal	—	Space.instFiniteDimensionalReal Space.instBorelSpace Space.inner_eq_sum sum_fun const_fun_smul mono Space.eval_continuous Space.abs_eval_le_norm
isDistBounded_smul_self 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instSMulReal	—	congr norm_mul_isDistBounded Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
isDistBounded_smul_self_repr 📖	mathematical	Space.IsDistBounded	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	congr norm_mul_isDistBounded Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
log_norm 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	mono fun_add inv norm Space.instFiniteDimensionalReal Space.instBorelSpace
mono 📖	—	Space.IsDistBounded Space Space.instMeasurableSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instBorelSpace	—	—	Space.instFiniteDimensionalReal Space.instBorelSpace
mul_const_fun 📖	—	Space.IsDistBounded	—	—	const_smul
mul_inner_pow_neg_two 📖	mathematical	—	Space.IsDistBounded Space Space.instInnerReal Space.instNorm	—	mono const_mul_fun congr pow Space.instFiniteDimensionalReal Space.instBorelSpace
nat_pow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	pow
nat_pow_shift 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup	—	pow_shift
neg 📖	—	Space.IsDistBounded	—	—	const_smul
norm 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	nat_pow
norm_add 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instAdd	—	nat_pow_shift
norm_add_nat_pow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	sum_fun mul_const_fun nat_pow
norm_add_pos_nat_zpow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	norm_add_nat_pow mono const Space.instFiniteDimensionalReal Space.instBorelSpace
norm_mul_isDistBounded 📖	mathematical	Space.IsDistBounded	Space Space.instNorm	—	norm_smul_isDistBounded
norm_smul_isDistBounded 📖	mathematical	Space.IsDistBounded	Space Space.instNorm	—	Space.instFiniteDimensionalReal Space.instBorelSpace mono congr sum_fun const_mul_fun norm_smul_zpow
norm_smul_nat_pow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instAdd	—	mono sum_fun mul_const_fun nat_pow Space.instFiniteDimensionalReal Space.instBorelSpace
norm_smul_zpow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instAdd	—	norm_smul_nat_pow mono const Space.instFiniteDimensionalReal Space.instBorelSpace pow add const_mul_fun comp_sub_right
norm_sub 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup	—	nat_pow_shift
pi_comp 📖	—	Space.IsDistBounded	—	—	Space.instFiniteDimensionalReal Space.instBorelSpace
pow 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm	—	Space.instFiniteDimensionalReal Space.instBorelSpace
pow_shift 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup	—	Space.instFiniteDimensionalReal Space.instBorelSpace
smul_const 📖	—	Space.IsDistBounded	—	—	congr mul_const_fun Space.instFiniteDimensionalReal Space.instBorelSpace aestronglyMeasurable
sum 📖	mathematical	Space.IsDistBounded	Space	—	zero add
sum_fun 📖	—	Space.IsDistBounded	—	—	sum
vector_component 📖	—	Space.IsDistBounded Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup	—	—	Space.instFiniteDimensionalReal Space.instBorelSpace Lorentz.Vector.coord_continuous
zero 📖	mathematical	—	Space.IsDistBounded Space	—	Space.instFiniteDimensionalReal Space.instBorelSpace
zpow_smul_repr_self 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	congr zpow_smul_self Space.instFiniteDimensionalReal Space.instBorelSpace
zpow_smul_repr_self_sub 📖	mathematical	—	Space.IsDistBounded Space Space.instNorm Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	comp_sub_right zpow_smul_repr_self
zpow_smul_self 📖	mathematical	—	Space.IsDistBounded Space Space.instNormedAddCommGroup Space.instSMulReal Space.instNorm	—	mono const Space.instFiniteDimensionalReal Space.instBorelSpace congr pow

---

← Back to Index