We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 898eace commit 7ca8bd0Copy full SHA for 7ca8bd0
1 file changed
Mathlib/Analysis/Fourier/AddCircleMulti.lean
@@ -216,11 +216,6 @@ theorem coeFn_mFourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : d → ℤ) :
216
mFourierLp p n =ᵐ[volume] mFourier n :=
217
ContinuousMap.coeFn_toLp volume (mFourier n)
218
219
--- shortcut instance: avoids `synthInstance.maxHeartbeats` issue in `span_mFourierLp_closure_eq_top`
220
-instance {p : ℝ≥0∞} [Fact (1 ≤ p)] :
221
- ContinuousSMul ℂ (Lp ℂ p (volume : Measure (UnitAddTorus d))) :=
222
- inferInstance
223
-
224
/-- For each `1 ≤ p < ∞`, the linear span of the monomials `mFourier n` is dense in the `Lᵖ` space
225
of functions on `UnitAddTorus d`. -/
226
theorem span_mFourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
0 commit comments