BorelCaratheodory

📁 Source: PrimeNumberTheoremAnd/BorelCaratheodory.lean

Statistics

Metric	Count
Definitions divRemovable_zero, schwartzQuotient	2
Theorems norm_le_of_norm_le_on_sphere, schwartzQuotient, AnalyticOn_divRemovable_zero, AnalyticOn_divRemovable_zero_closedBall, norm_le_norm_two_mul_sub_of_re_le, borelCaratheodory_closedBall, divRemovable_zero_of_ne_zero	7
Total	9

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le_of_norm_le_on_sphere 📖	—	—	—	—	—
schwartzQuotient 📖	mathematical	—	schwartzQuotient	—	AnalyticOn_divRemovable_zero_closedBall

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_le_norm_two_mul_sub_of_re_le 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
divRemovable_zero 📖	CompOp	3 math math: AnalyticOn_divRemovable_zero, divRemovable_zero_of_ne_zero, AnalyticOn_divRemovable_zero_closedBall
schwartzQuotient 📖	CompOp	1 math math: AnalyticOn.schwartzQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AnalyticOn_divRemovable_zero 📖	mathematical	—	divRemovable_zero	—	—
AnalyticOn_divRemovable_zero_closedBall 📖	mathematical	—	divRemovable_zero	—	divRemovable_zero_of_ne_zero AnalyticOn_divRemovable_zero
borelCaratheodory_closedBall 📖	—	—	—	—	divRemovable_zero_of_ne_zero Complex.norm_le_norm_two_mul_sub_of_re_le AnalyticOn.norm_le_of_norm_le_on_sphere AnalyticOn.schwartzQuotient
divRemovable_zero_of_ne_zero 📖	mathematical	—	divRemovable_zero	—	—

---

← Back to Index