Norm

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

Statistics

Metric	Count
Definitions `normPowerSeries`	1
Theorems `normPowerSeries_deriv`, `normPowerSeries_fderiv`, `normPowerSeries_inv`, `normPowerSeries_log`, `normPowerSeries_single`, `normPowerSeries_zpow`, `deriv_log_normPowerSeries`, `deriv_normPowerSeries`, `deriv_normPowerSeries_tendsto`, `deriv_normPowerSeries_zpow`, `differentiable_log_normPowerSeries`, `differentiable_normPowerSeries_inv`, `differentiable_normPowerSeries_zpow`, `distDiv_inv_pow_eq_dim`, `distGrad_distOfFunction_log_norm`, `distGrad_distOfFunction_norm_zpow`, `fderiv_log_normPowerSeries`, `fderiv_normPowerSeries`, `fderiv_normPowerSeries_tendsto`, `fderiv_normPowerSeries_zpow`, `gradient_dist_normPowerSeries_log`, `gradient_dist_normPowerSeries_log_tendsTo`, `gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm`, `gradient_dist_normPowerSeries_zpow`, `gradient_dist_normPowerSeries_zpow_tendsTo`, `gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm`, `normPowerSeries_aestronglyMeasurable`, `normPowerSeries_differentiable`, `normPowerSeries_eq`, `normPowerSeries_eq_rpow`, `normPowerSeries_inv_le`, `normPowerSeries_inv_tendsto`, `normPowerSeries_le_norm_sq_add_one`, `normPowerSeries_log_le`, `normPowerSeries_log_le_normPowerSeries`, `normPowerSeries_ne_zero`, `normPowerSeries_nonneg`, `normPowerSeries_pos`, `normPowerSeries_tendsto`, `normPowerSeries_zpow_le_norm_sq_add_one`, `norm_le_normPowerSeries`, `norm_lt_normPowerSeries`	42
Total	43

Space

Definitions

Name	Category	Theorems
`normPowerSeries` 📖	CompOp	38 math math: `norm_le_normPowerSeries`, `IsDistBounded.normPowerSeries_single`, `gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm`, `normPowerSeries_log_le_normPowerSeries`, `differentiable_normPowerSeries_inv`, `differentiable_log_normPowerSeries`, `IsDistBounded.normPowerSeries_deriv`, `normPowerSeries_tendsto`, `gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm`, `normPowerSeries_differentiable`, `normPowerSeries_log_le`, `deriv_normPowerSeries_tendsto`, `normPowerSeries_inv_le`, `normPowerSeries_eq_rpow`, `IsDistBounded.normPowerSeries_zpow`, `gradient_dist_normPowerSeries_log`, `gradient_dist_normPowerSeries_zpow_tendsTo`, `fderiv_normPowerSeries_zpow`, `norm_lt_normPowerSeries`, `gradient_dist_normPowerSeries_zpow`, `normPowerSeries_eq`, `normPowerSeries_pos`, `IsDistBounded.normPowerSeries_log`, `deriv_normPowerSeries`, `deriv_normPowerSeries_zpow`, `normPowerSeries_aestronglyMeasurable`, `normPowerSeries_le_norm_sq_add_one`, `differentiable_normPowerSeries_zpow`, `IsDistBounded.normPowerSeries_fderiv`, `fderiv_normPowerSeries`, `normPowerSeries_inv_tendsto`, `normPowerSeries_zpow_le_norm_sq_add_one`, `fderiv_normPowerSeries_tendsto`, `deriv_log_normPowerSeries`, `IsDistBounded.normPowerSeries_inv`, `gradient_dist_normPowerSeries_log_tendsTo`, `normPowerSeries_nonneg`, `fderiv_log_normPowerSeries`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv_log_normPowerSeries` 📖	mathematical	—	`deriv` `normPowerSeries` `val`	—	`deriv_eq_fderiv_basis` `normPowerSeries_ne_zero` `normPowerSeries_differentiable` `fderiv_normPowerSeries` `basis_inner`
`deriv_normPowerSeries` 📖	mathematical	—	`deriv` `normPowerSeries` `val`	—	`deriv_eq_fderiv_basis` `normPowerSeries_eq` `deriv_norm_sq`
`deriv_normPowerSeries_tendsto` 📖	mathematical	—	`deriv` `normPowerSeries` `val` `Space` `instNorm`	—	`deriv_normPowerSeries` `normPowerSeries_inv_tendsto`
`deriv_normPowerSeries_zpow` 📖	mathematical	—	`deriv` `normPowerSeries` `val`	—	`deriv_eq_fderiv_basis` `normPowerSeries_ne_zero` `normPowerSeries_differentiable` `fderiv_normPowerSeries` `basis_inner`
`differentiable_log_normPowerSeries` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `normPowerSeries`	—	`normPowerSeries_differentiable` `normPowerSeries_ne_zero`
`differentiable_normPowerSeries_inv` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `normPowerSeries`	—	`differentiable_normPowerSeries_zpow`
`differentiable_normPowerSeries_zpow` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `normPowerSeries`	—	`normPowerSeries_differentiable` `normPowerSeries_ne_zero`
`distDiv_inv_pow_eq_dim` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDiv` `distOfFunction` `instNorm` `basis` `IsDistBounded.zpow_smul_repr_self` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace` `instSeminormedAddCommGroup` `instZero` `Distribution.diracDelta`	—	`IsDistBounded.zpow_smul_repr_self` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction.congr_simp` `distDiv_ofFunction` `grad_inner_space_unit_vector` `instNontrivialSucc` `integrable_isDistBounded_inner_grad_schwartzMap_spherical` `IsDistBounded.inv_pow_smul_repr_self` `finrank_eq_dim`
`distGrad_distOfFunction_log_norm` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `instNorm` `IsDistBounded.log_norm` `basis` `IsDistBounded.zpow_smul_repr_self`	—	`IsDistBounded.log_norm` `IsDistBounded.zpow_smul_repr_self` `IsDistBounded.normPowerSeries_log` `gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm` `gradient_dist_normPowerSeries_log_tendsTo`
`distGrad_distOfFunction_norm_zpow` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `instNorm` `IsDistBounded.pow` `basis` `IsDistBounded` `IsDistBounded.const_fun_smul` `IsDistBounded.zpow_smul_repr_self`	—	`IsDistBounded.pow` `IsDistBounded.const_fun_smul` `IsDistBounded.zpow_smul_repr_self` `IsDistBounded.normPowerSeries_zpow` `gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm` `gradient_dist_normPowerSeries_zpow_tendsTo`
`fderiv_log_normPowerSeries` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `normPowerSeries` `instInnerReal`	—	`fderiv_eq_sum_deriv` `inner_eq_sum` `deriv_log_normPowerSeries`
`fderiv_normPowerSeries` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `normPowerSeries` `instInnerReal`	—	`fderiv_eq_sum_deriv` `inner_eq_sum` `deriv_normPowerSeries`
`fderiv_normPowerSeries_tendsto` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `normPowerSeries` `instInnerReal` `instNorm`	—	`fderiv_normPowerSeries` `normPowerSeries_inv_tendsto`
`fderiv_normPowerSeries_zpow` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `normPowerSeries` `instInnerReal`	—	`fderiv_eq_sum_deriv` `inner_eq_sum` `deriv_normPowerSeries_zpow`
`gradient_dist_normPowerSeries_log` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_log` `basis` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.normPowerSeries_zpow`	—	`IsDistBounded.normPowerSeries_log` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.normPowerSeries_zpow` `instFiniteDimensionalReal` `distGrad_inner_eq` `distOfFunction.congr_simp` `Distribution.fderivD_apply` `instBorelSpace` `distOfFunction_apply` `distOfFunction_inner` `IsDistBounded.integrable_space_fderiv_mul` `IsDistBounded.integrable_space_mul` `fderiv_log_normPowerSeries` `IsDistBounded.isDistBounded_mul_inner` `differentiable_log_normPowerSeries` `basis_repr_inner_eq`
`gradient_dist_normPowerSeries_log_tendsTo` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_log` `instNorm` `basis` `IsDistBounded.zpow_smul_repr_self`	—	`IsDistBounded.normPowerSeries_log` `IsDistBounded.zpow_smul_repr_self` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.normPowerSeries_zpow` `gradient_dist_normPowerSeries_log` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_inner` `IsDistBounded.aeStronglyMeasurable_schwartzMap_smul` `basis_repr_inner_eq` `IsDistBounded.isDistBounded_mul_inner'` `IsDistBounded.integrable_space_mul` `IsDistBounded.add` `IsDistBounded.norm_add_pos_nat_zpow` `IsDistBounded.mul_inner_pow_neg_two` `instNontrivialSucc` `normPowerSeries_zpow_le_norm_sq_add_one` `normPowerSeries_tendsto`
`gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_log` `instNorm` `IsDistBounded.log_norm`	—	`IsDistBounded.normPowerSeries_log` `IsDistBounded.log_norm` `instFiniteDimensionalReal` `instBorelSpace` `distGrad_inner_eq` `Distribution.fderivD_apply` `IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul` `IsDistBounded.integrable_space_fderiv` `IsDistBounded.add` `IsDistBounded.inv` `IsDistBounded.fun_add` `IsDistBounded.norm` `IsDistBounded.const` `instNontrivialSucc` `normPowerSeries_log_le` `normPowerSeries_tendsto`
`gradient_dist_normPowerSeries_zpow` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_zpow` `basis` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.const_mul_fun`	—	`IsDistBounded.normPowerSeries_zpow` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.const_mul_fun` `instFiniteDimensionalReal` `distGrad_inner_eq` `Distribution.fderivD_apply` `instBorelSpace` `distOfFunction_apply` `distOfFunction_inner` `IsDistBounded.integrable_space_fderiv_mul` `IsDistBounded.integrable_space_mul` `fderiv_normPowerSeries_zpow` `IsDistBounded.isDistBounded_mul_inner` `differentiable_normPowerSeries_zpow` `basis_repr_inner_eq`
`gradient_dist_normPowerSeries_zpow_tendsTo` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_zpow` `instNorm` `basis` `IsDistBounded` `IsDistBounded.const_fun_smul` `IsDistBounded.zpow_smul_repr_self`	—	`IsDistBounded.normPowerSeries_zpow` `IsDistBounded.const_fun_smul` `IsDistBounded.zpow_smul_repr_self` `IsDistBounded.isDistBounded_smul_self_repr` `IsDistBounded.const_mul_fun` `gradient_dist_normPowerSeries_zpow` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_inner` `IsDistBounded.aeStronglyMeasurable_schwartzMap_smul` `basis_repr_inner_eq` `IsDistBounded.isDistBounded_mul_inner'` `IsDistBounded.integrable_space_mul` `IsDistBounded.add` `IsDistBounded.norm_add_pos_nat_zpow` `IsDistBounded.isDistBounded_mul_inner_of_smul_norm` `IsDistBounded.mono` `IsDistBounded.pow` `IsDistBounded.const` `instNontrivialSucc` `normPowerSeries_zpow_le_norm_sq_add_one` `normPowerSeries_tendsto`
`gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distGrad` `distOfFunction` `normPowerSeries` `IsDistBounded.normPowerSeries_zpow` `instNorm` `IsDistBounded.pow`	—	`IsDistBounded.normPowerSeries_zpow` `IsDistBounded.pow` `instFiniteDimensionalReal` `instBorelSpace` `distGrad_inner_eq` `Distribution.fderivD_apply` `IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul` `IsDistBounded.integrable_space_fderiv` `IsDistBounded.add` `IsDistBounded.norm_add_pos_nat_zpow` `instNontrivialSucc` `normPowerSeries_zpow_le_norm_sq_add_one` `normPowerSeries_tendsto`
`normPowerSeries_aestronglyMeasurable` 📖	mathematical	—	`Space` `instMeasurableSpace` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instFiniteDimensionalReal` `instBorelSpace` `normPowerSeries`	—	`instFiniteDimensionalReal` `instBorelSpace` `normPowerSeries_eq_rpow`
`normPowerSeries_differentiable` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `normPowerSeries`	—	`normPowerSeries_eq_rpow`
`normPowerSeries_eq` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	—
`normPowerSeries_eq_rpow` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_eq`
`normPowerSeries_inv_le` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	—
`normPowerSeries_inv_tendsto` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_tendsto`
`normPowerSeries_le_norm_sq_add_one` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_eq`
`normPowerSeries_log_le` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_log_le_normPowerSeries` `normPowerSeries_inv_le` `normPowerSeries_le_norm_sq_add_one`
`normPowerSeries_log_le_normPowerSeries` 📖	mathematical	—	`normPowerSeries`	—	—
`normPowerSeries_ne_zero` 📖	—	—	—	—	`normPowerSeries_eq`
`normPowerSeries_nonneg` 📖	mathematical	—	`normPowerSeries`	—	`normPowerSeries_eq`
`normPowerSeries_pos` 📖	mathematical	—	`normPowerSeries`	—	`normPowerSeries_eq`
`normPowerSeries_tendsto` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_eq_rpow`
`normPowerSeries_zpow_le_norm_sq_add_one` 📖	mathematical	—	`normPowerSeries` `Space` `instNorm`	—	`normPowerSeries_le_norm_sq_add_one` `norm_le_normPowerSeries`
`norm_le_normPowerSeries` 📖	mathematical	—	`Space` `instNorm` `normPowerSeries`	—	`normPowerSeries_eq`
`norm_lt_normPowerSeries` 📖	mathematical	—	`Space` `instNorm` `normPowerSeries`	—	`normPowerSeries_eq`

Space.IsDistBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normPowerSeries_deriv` 📖	mathematical	—	`Space.IsDistBounded` `Space.deriv` `Space.normPowerSeries`	—	`Space.deriv_normPowerSeries` `component_mul_isDistBounded` `normPowerSeries_inv`
`normPowerSeries_fderiv` 📖	mathematical	—	`Space.IsDistBounded` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommGroup` `Space.instModuleReal` `Space.normPowerSeries`	—	`Space.fderiv_eq_sum_deriv` `sum_fun` `const_fun_smul` `normPowerSeries_deriv`
`normPowerSeries_inv` 📖	mathematical	—	`Space.IsDistBounded` `Space.normPowerSeries`	—	`normPowerSeries_zpow`
`normPowerSeries_log` 📖	mathematical	—	`Space.IsDistBounded` `Space.normPowerSeries`	—	`mono` `fun_add` `normPowerSeries_inv` `normPowerSeries_single` `Space.instFiniteDimensionalReal` `Space.instBorelSpace` `Space.normPowerSeries_aestronglyMeasurable` `Space.normPowerSeries_log_le_normPowerSeries`
`normPowerSeries_single` 📖	mathematical	—	`Space.IsDistBounded` `Space.normPowerSeries`	—	`normPowerSeries_zpow`
`normPowerSeries_zpow` 📖	mathematical	—	`Space.IsDistBounded` `Space.normPowerSeries`	—	`mono` `norm_add_nat_pow` `Space.instFiniteDimensionalReal` `Space.instBorelSpace` `Space.normPowerSeries_aestronglyMeasurable` `Space.normPowerSeries_le_norm_sq_add_one` `const` `Space.normPowerSeries_eq_rpow` `Space.normPowerSeries_eq`

---

← Back to Index