Source indexedlemma · leanprover/lean4:v4.32.0

carlesonOperatorReal_eq_of_restrict_interval

Carleson.Classical.CarlesonOperatorReal · Carleson/Classical/CarlesonOperatorReal.lean:283 to 303

Mathematical statement

Exact Lean statement

lemma carlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b : ℝ} {x : ℝ}
  (hx : x ∈ Set.Icc a b) :
    T f x = T ((Set.Ioo (a - 1) (b + 1)).indicator f) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma carlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b : ℝ} {x : ℝ}  (hx : x ∈ Set.Icc a b) :    T f x = T ((Set.Ioo (a - 1) (b + 1)).indicator f) x := by  simp_rw [carlesonOperatorReal]  congr with n  congr with _  congr with _  congr with _  congr with y  rw [mul_eq_mul_right_iff, mul_eq_mul_right_iff]  left  rw [Set.indicator]  split_ifs with hy  · left; rfl  · right    apply k_of_one_le_abs    simp only [Set.mem_Ioo, not_and_or, not_lt] at hy    rw [le_abs]    rcases hy with hy | hy    · left; linarith [hx.1]    · right; linarith [hx.2]