Documentation

Carleson.Classical.CarlesonOnTheRealLine

@[reducible]

def DoublingMeasureR2 :

MeasureTheory.DoublingMeasure ℝ 2

Equations

DoublingMeasureR2 = MeasureTheory.DoublingMeasure.mono DoublingMeasureR2.proof_2

Instances For

instance DoublingMeasureR4 :

MeasureTheory.DoublingMeasure ℝ ↑(2 ^ 4)

Equations

DoublingMeasureR4 = MeasureTheory.DoublingMeasure.mono DoublingMeasureR4.proof_2

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 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) ≤ dist f g

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

dist f g ≤ dist f g

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

dist f g ≤ 2 * dist f g

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

2 * dist f g ≤ dist f g

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

CoveredByBalls (Metric.ball 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)

Equations

real_van_der_Corput = ⋯

theorem Real.vol_real_eq {x y : ℝ} :

Real.vol x y = 2 * |x - y|

theorem Real.vol_real_symm {x y : ℝ} :

Real.vol x y = Real.vol y x

instance isOneSidedKernelHilbert :

IsOneSidedKernel 4 K

Equations

isOneSidedKernelHilbert = ⋯

instance isTwoSidedKernelHilbert :

IsTwoSidedKernel 4 K

Equations

isTwoSidedKernelHilbert = ⋯

theorem Hilbert_strong_2_2 (r : ℝ) :

r > 0 → MeasureTheory.HasBoundedStrongType (CZOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts 4)

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 ≤ ENNReal.ofReal (C10_0_1 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹