Documentation

Carleson.Classical.CarlesonOnTheRealLine

theorem localOscillation_on_emptyset {X : Type} [PseudoMetricSpace X] {f g : C(X, ℝ )} :

localOscillation ∅ f g = 0

theorem localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f g : C(X, ℝ )} {R : ℝ} (R_nonpos : R ≤ 0) :

localOscillation (Metric.ball x R) f g = 0

def integer_linear (n : ℤ) :

Equations

integer_linear n = { toFun := fun (x : ℝ) => ↑n * x, continuous_toFun := ⋯ }

Instances For

instance instFunctionDistancesReal :

FunctionDistances ℝ ℝ

Equations

One or more equations did not get rendered due to their size.

theorem dist_integer_linear_eq {n m : Θ ℝ} {x R : ℝ} :

dist_{x ,R} n m = 2 * (R ⊔ 0) * |↑n - ↑m|

theorem coeΘ_R (n : Θ ℝ) (x : ℝ) :

n x = ↑n * x

theorem coeΘ_R_C (n : Θ ℝ) (x : ℝ) :

↑(n x) = ↑n * ↑x

theorem oscillation_control {x r : ℝ} {f g : Θ ℝ} :

localOscillation (Metric.ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x ,r} f g)

theorem frequency_monotone {x₁ x₂ r R : ℝ} {f g : Θ ℝ} (h : Metric.ball x₁ r ⊆ Metric.ball x₂ R) :

dist_{x₁ ,r} f g ≤ dist_{x₂ ,R} f g

theorem frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} :

dist_{x₂ ,2 * r} f g ≤ 2 * dist_{x₁ ,r} f g

theorem frequency_ball_growth {x₁ x₂ r : ℝ} {f g : Θ ℝ} :

2 * dist_{x₁ ,r} f g ≤ dist_{x₂ ,2 * r} f g

theorem integer_ball_cover {x R R' : ℝ} {f : WithFunctionDistance x R} :

CoveredByBalls (ball_{x ,R} f (2 * R')) 3 R'

instance compatibleFunctions_R :

CompatibleFunctions ℝ ℝ (2 ^ 4)

Equations

compatibleFunctions_R = CompatibleFunctions.mk compatibleFunctions_R.proof_1 ⋯ ⋯ @compatibleFunctions_R.proof_2 @compatibleFunctions_R.proof_3 @compatibleFunctions_R.proof_4

instance real_van_der_Corput :

IsCancellative ℝ (defaultτ 4)

theorem Real.vol_real_eq {x y : ℝ} :

vol x y = 2 * |x - y|

theorem Real.vol_real_symm {x y : ℝ} :

vol x y = vol y x

instance isOneSidedKernelHilbert :

IsOneSidedKernel 4 K

instance isTwoSidedKernelHilbert :

IsTwoSidedKernel 4 K

theorem carlesonOperatorReal_le_carlesonOperator :

carlesonOperatorReal K ≤ carlesonOperator K

theorem rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x) :

∫⁻ (x : ℝ) in G, carlesonOperatorReal K f x ≤ ↑(C10_0_1 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹