Source indexedlemma · leanprover/lean4:v4.32.0

domain_reformulation

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:170 to 211

Mathematical statement

Exact Lean statement

lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-π) (3 * π)) {N : ℕ}
    {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :
    ∫ (y : ℝ) in x - π..x + π, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
    = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1},
        g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-π) (3 * π)) {N : ℕ}    {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :    ∫ (y : ℝ) in x - π..x + π, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))    = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1},        g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by  calc _    _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 π}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by      rw [annulus_real_eq (le_refl 0),        setIntegral_union (by simp) measurableSet_Ioo, ← integral_Ioc_eq_integral_Ioo,        ← setIntegral_union (Set.disjoint_of_subset_right Set.Ioo_subset_Ioc_self (by simp)) measurableSet_Ioo,        intervalIntegral.integral_of_le (by linarith [pi_pos]), integral_Ioc_eq_integral_Ioo,        sub_zero, add_zero, Set.Ioc_union_Ioo_eq_Ioo (by linarith [pi_pos]) (by linarith [pi_pos])]      --TODO: Many similar goals => improve this further?      · rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith [pi_pos])]        apply (intervalIntegrable_mul_dirichletKernel'_max hx hg).mono_set        rw [Set.uIcc_of_le (by linarith [pi_pos]), Set.uIcc_of_le (by linarith [pi_pos])]        apply Set.Icc_subset_Icc_right (by linarith [pi_pos])      all_goals        rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [pi_pos])]        apply (intervalIntegrable_mul_dirichletKernel'_max hx hg).mono_set        rw [Set.uIcc_of_le (by linarith [pi_pos]), Set.uIcc_of_le (by linarith [pi_pos])]      · apply Set.Icc_subset_Icc_left (by linarith [pi_pos])      · apply Set.Icc_subset_Icc_right (by linarith [pi_pos])      · apply Set.Icc_subset_Icc_left (by linarith [pi_pos])    _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by      rw [←integral_indicator annulus_measurableSet, ←integral_indicator annulus_measurableSet]      congr with y      rw [Set.indicator_apply, Set.indicator_apply, Dirichlet_Hilbert_eq]      split_ifs with h₀ h₁ h₂      · trivial      · dsimp at h₀ h₁        rw [Real.dist_eq, Set.mem_Ioo] at h₀ h₁        push Not at h₁        rw [k_of_one_le_abs (h₁ h₀.1)]        simp      · rw [k_of_one_le_abs]        · simp        dsimp at h₀ h₂        rw [Real.dist_eq, Set.mem_Ioo] at h₀ h₂        push Not at h₀        exact le_trans' (h₀ h₂.1) (by linarith [Real.two_le_pi])      · trivial