Theorem: integrable_annulus (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
rw [← MeasureTheory.IntegrableOn, annulus_real_eq r_nonneg]
State after:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x - 1) (x - r) ∪ Set.Ioo (x + r) (x + 1)) MeasureTheory.volume

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x - 1) (x - r) ∪ Set.Ioo (x + r) (x + 1)) MeasureTheory.volume
Tactic:
apply MeasureTheory.IntegrableOn.union <;>
. rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
  apply hf.mono_set
  rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
  intro y hy
  constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
State after:
no goals

State before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ MeasureTheory.IntegrableOn (fun x => f x) (Set.Ioo (x + r) (x + 1)) MeasureTheory.volume
Tactic:
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
State after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ IntervalIntegrable (fun x => f x) MeasureTheory.volume (x + r) (x + 1)

State before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ IntervalIntegrable (fun x => f x) MeasureTheory.volume (x + r) (x + 1)
Tactic:
apply hf.mono_set
State after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.uIcc (x + r) (x + 1) ⊆ Set.uIcc (-Real.pi) (3 * Real.pi)

State before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.uIcc (x + r) (x + 1) ⊆ Set.uIcc (-Real.pi) (3 * Real.pi)
Tactic:
rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
State after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.Icc (x + r) (x + 1) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)

State before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ Set.Icc (x + r) (x + 1) ⊆ Set.Icc (-Real.pi) (3 * Real.pi)
Tactic:
intro y hy
State after:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
y : ℝ
hy : y ∈ Set.Icc (x + r) (x + 1)
⊢ y ∈ Set.Icc (-Real.pi) (3 * Real.pi)

State before:
case ht
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
y : ℝ
hy : y ∈ Set.Icc (x + r) (x + 1)
⊢ y ∈ Set.Icc (-Real.pi) (3 * Real.pi)
Tactic:
constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
State after:
no goals

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ x + r ≤ x + 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
r : ℝ
r_nonneg : 0 ≤ r
rle1 : r < 1
⊢ -Real.pi ≤ 3 * Real.pi
Tactic:
linarith [Real.pi_pos]
State after:
no goals