internlm/Lean-Github huggingface dataset:
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case e_f
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ (fun x => T' f x) = fun a => ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
ext x
Proof state after:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ T' f x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ T' f x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
rw [CarlesonOperatorReal'_mul δpos]
Proof state after:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ↑δ.toNNReal * T' (fun x => 1 / ↑δ * f x) x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ↑δ.toNNReal * T' (fun x => 1 / ↑δ * f x) x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
congr
Proof state after:
case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
exact ENNReal.ofReal_ne_top
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹)
Tactic:
gcongr
Proof state after:
case bc
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case bc
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
apply rcarleson' measurableSetF measurableSetE
Proof state after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∀ (x : ℝ), ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∀ (x : ℝ), ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Tactic:
intro x
Proof state after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Tactic:
simp
Proof state after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ |δ|⁻¹ * Complex.abs (f x) ≤ F.indicator 1 x
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ |δ|⁻¹ * Complex.abs (f x) ≤ F.indicator 1 x
Tactic:
rw [_root_.abs_of_nonneg δpos.le, inv_mul_le_iff δpos]
Proof state after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ Complex.abs (f x) ≤ δ * F.indicator 1 x
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ Complex.abs (f x) ≤ δ * F.indicator 1 x
Tactic:
exact hf x
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal (δ * C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
rw [ENNReal.ofReal_mul δpos.le]
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal δ * ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal δ * ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
ring
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E ^ 2⁻¹
Tactic:
rw [ENNReal.ofReal_mul (by apply mul_nonneg δpos.le; rw [C1_2]; norm_num), ← ENNReal.ofReal_rpow_of_pos (by linarith [Real.pi_pos])]
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * ENNReal.ofReal (4 * Real.pi) ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * ENNReal.ofReal (4 * Real.pi) ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
convert rcarleson_exceptional_set_estimate δpos measurableSet_Icc hf measurableSetE hE
Proof state after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = MeasureTheory.volume (Set.Icc (-Real.pi) (3 * Real.pi))
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = MeasureTheory.volume (Set.Icc (-Real.pi) (3 * Real.pi))
Tactic:
rw [Real.volume_Icc]
Proof state after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = ENNReal.ofReal (3 * Real.pi - -Real.pi)
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = ENNReal.ofReal (3 * Real.pi - -Real.pi)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ δ * C1_2 4 2
Tactic:
apply mul_nonneg δpos.le
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ C1_2 4 2
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ C1_2 4 2
Tactic:
rw [C1_2]
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ 2 ^ (450 * 4 ^ 3) / (2 - 1) ^ 5
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ 2 ^ (450 * 4 ^ 3) / (2 - 1) ^ 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate_specific
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 < 4 * Real.pi
Tactic:
linarith [Real.pi_pos]
Proof state after:
no goals
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C_control_approximation_effect ε
Tactic:
rw [C_control_approximation_effect]
Proof state after:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi
Tactic:
apply lt_add_of_pos_of_le _ (by rfl)
Proof state after:
ε : ℝ
εpos : 0 < ε
⊢ 0 < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
apply mul_pos (C1_2_pos (by norm_num))
Proof state after:
ε : ℝ
εpos : 0 < ε
⊢ 0 < (8 / (Real.pi * ε)) ^ 2⁻¹
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8 / (Real.pi * ε)
Theorem: lt_C_control_approximation_effect
Proof state before:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8 / (Real.pi * ε)
Tactic:
apply div_pos (by norm_num)
Proof state after:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < Real.pi * ε
Theorem: lt_C_control_approximation_effect
Proof state before:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < Real.pi * ε
Tactic:
apply mul_pos Real.pi_pos εpos
Proof state after:
no goals
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi ≤ Real.pi
Tactic:
rfl
Proof state after:
no goals
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt_C_control_approximation_effect
Proof state before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: C_control_approximation_effect_eq
Proof state before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C_control_approximation_effect ε * δ = δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ
Tactic:
symm
Proof state after:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ = C_control_approximation_effect ε * δ
Theorem: C_control_approximation_effect_eq
Proof state before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ = C_control_approximation_effect ε * δ
Tactic:
rw [C_control_approximation_effect, mul_comm, mul_div_right_comm, mul_comm δ, mul_assoc, mul_comm δ, ← mul_assoc, ← mul_assoc, ← add_mul]
Proof state after:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ ((2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ + Real.pi) * δ =
    (C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi) * δ
Theorem: C_control_approximation_effect_eq
Proof state before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ ((2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ + Real.pi) * δ =
    (C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi) * δ
Tactic:
congr 2
Proof state after:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
rw [mul_comm _ (C1_2 4 2), mul_assoc]
Proof state after:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C1_2 4 2 * ((2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹) = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C1_2 4 2 * ((2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹) = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
congr
Proof state after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹ = (8 / (Real.pi * ε)) ^ 2⁻¹
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹ = (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
rw [Real.div_rpow, Real.div_rpow _ (mul_nonneg _ _), Real.mul_rpow, Real.mul_rpow]
Proof state after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ 2⁻¹ / ε ^ 2⁻¹ / Real.pi * (4 ^ 2⁻¹ * Real.pi ^ 2⁻¹) = 8 ^ 2⁻¹ / (Real.pi ^ 2⁻¹ * ε ^ 2⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ 2⁻¹ / ε ^ 2⁻¹ / Real.pi * (4 ^ 2⁻¹ * Real.pi ^ 2⁻¹) = 8 ^ 2⁻¹ / (Real.pi ^ 2⁻¹ * ε ^ 2⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
ring_nf
Proof state after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ (1 / 2) * (ε ^ (1 / 2))⁻¹ * Real.pi⁻¹ * 4 ^ (1 / 2) * Real.pi ^ (1 / 2) =
    (ε ^ (1 / 2))⁻¹ * 8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ (1 / 2) * (ε ^ (1 / 2))⁻¹ * Real.pi⁻¹ * 4 ^ (1 / 2) * Real.pi ^ (1 / 2) =
    (ε ^ (1 / 2))⁻¹ * 8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
rw [mul_assoc, mul_comm (2 ^ _), mul_assoc, mul_assoc, mul_assoc, mul_comm (4 ^ _), ← mul_assoc Real.pi⁻¹,
    ← Real.rpow_neg_one Real.pi, ← Real.rpow_add, mul_comm (Real.pi ^ _), ← mul_assoc (2 ^ _), ← Real.mul_rpow]
Proof state after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (ε ^ (1 / 2))⁻¹ * ((2 * 4) ^ (1 / 2) * Real.pi ^ (-1 + 1 / 2)) =
    (ε ^ (1 / 2))⁻¹ * (8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (ε ^ (1 / 2))⁻¹ * ((2 * 4) ^ (1 / 2) * Real.pi ^ (-1 + 1 / 2)) =
    (ε ^ (1 / 2))⁻¹ * (8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
congr
Proof state after:
case e_a.e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 * 4 = 8

case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 * 4 = 8

case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
norm_num
Proof state after:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε