Carleson Operator Real mul
carlesonOperatorReal_mul
Plain-language statement
The real-line Carleson operator is positively homogeneous. For every ,
where the scalar on the right is interpreted in the extended nonnegative reals.
Exact Lean statement
lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) :
T f x = ENNReal.ofReal a * T (fun x ↦ 1 / a * f x) xFormal artifact
Lean source
lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) : T f x = ENNReal.ofReal a * T (fun x ↦ 1 / a * f x) x := by rw [carlesonOperatorReal, carlesonOperatorReal, ENNReal.mul_iSup] congr with n rw [ENNReal.mul_iSup] congr with r rw [ENNReal.mul_iSup] congr ext rpos rw [ENNReal.mul_iSup] congr with rle1 norm_cast rw [← Real.enorm_eq_ofReal ha.le] simp_rw [ mul_assoc, show ∫ _ in _, _ = _ * ∫ y in _, f y * _ from integral_const_mul _ _, enorm_mul, ← mul_assoc, ← enorm_norm (Complex.ofReal (1 / a)), Complex.norm_real, enorm_norm, ← enorm_mul, mul_one_div_cancel ha.ne', enorm_one, one_mul ]- Project
- Carleson formalization
- License
- Apache-2.0
- Commit
- 74ef907d6bdb
- Source
- Carleson/Classical/CarlesonOperatorReal.lean:262-281
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Adjoint Carleson adjoint
adjointCarleson_adjoint
Plain-language statement
adjointCarleson is the adjoint of carlesonOn.
Source project: Carleson formalization
Person-level attribution pending.
Ae tendsto zero of distribution le
ae_tendsto_zero_of_distribution_le
Plain-language statement
Suppose that, for every error threshold and every measure tolerance , one can choose so that the set where exceeds has measure at most . Then converges to for almost every .
Source project: Carleson formalization
Person-level attribution pending.
Antichain operator
antichain_operator
Plain-language statement
For an antichain of pairwise incomparable tiles, and measurable functions and bounded by the indicators of and , the pairing of with the Carleson sum over is controlled by the norms of and and by positive powers of the two tile-density parameters. Concretely, the bound is
Source project: Carleson formalization
Person-level attribution pending.