Documentation

Carleson.Classical.CarlesonOnTheRealLineBasic

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_reducible]

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 * max 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_reducible]

instance compatibleFunctions_R :

CompatibleFunctions ℝ ℝ (2 ^ 4)

Equations

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

instance real_van_der_Corput :

IsCancellative ℝ (defaultτ 4)

theorem Real.vol_real_eq {x y : ℝ} :

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

theorem Real.vol_eq {x y : ℝ} :

vol x y = 2 * ‖x - y‖ₑ

theorem Real.vol_real_symm {x y : ℝ} :

Real.vol x y = Real.vol y x

theorem Real.vol_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