NormPow

📁 Source: PhysLean/SpaceAndTime/Space/Integrals/NormPow.lean

Statistics

Metric	Count
Definitions	0
Theorems integrableOn_norm_rpow_ball_compl_iff, integrableOn_norm_rpow_ball_iff, integrableOn_norm_rpow_iff_of_isBounded_nhds, integrableOn_norm_rpow_of_compl_nhds, integrableOn_norm_rpow_of_isBounded_compl_nhds, integrableOn_norm_rpow_shell	6
Total	6

Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrableOn_norm_rpow_ball_compl_iff 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm instPseudoMetricSpace instZero	—	instNontrivialSucc instFiniteDimensionalReal instBorelSpace finrank_eq_dim
integrableOn_norm_rpow_ball_iff 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm instPseudoMetricSpace instZero	—	instNontrivialSucc instFiniteDimensionalReal instBorelSpace finrank_eq_dim
integrableOn_norm_rpow_iff_of_isBounded_nhds 📖	mathematical	Space instPseudoMetricSpace instZero	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm	—	instFiniteDimensionalReal instBorelSpace integrableOn_norm_rpow_ball_iff
integrableOn_norm_rpow_of_compl_nhds 📖	mathematical	Space instPseudoMetricSpace instZero	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm	—	instFiniteDimensionalReal instBorelSpace integrableOn_norm_rpow_ball_compl_iff
integrableOn_norm_rpow_of_isBounded_compl_nhds 📖	mathematical	Space instPseudoMetricSpace instZero	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm	—	instFiniteDimensionalReal instBorelSpace integrableOn_norm_rpow_shell
integrableOn_norm_rpow_shell 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instFiniteDimensionalReal instMeasurableSpace instBorelSpace instNorm instPseudoMetricSpace instZero	—	instFiniteDimensionalReal instBorelSpace

---

← Back to Index