Theorem: Smooth1LeOne (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ (x : ℝ), 0 < x → Smooth1 Ψ ε x ≤ 1
Tactic:
unfold Smooth1 MellinConvolution DeltaSpike
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ (x : ℝ),
    0 < x → ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ (x : ℝ),
    0 < x → ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1
Tactic:
intro x xpos
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1
Tactic:
have := Smooth1LeOne_aux xpos εpos mass_one
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y ≤ 1
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, (fun y ↦ if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y) := ?_
  _ ≤ ∫ (y : ℝ) in Ioi 0, (Ψ ((x / y) ^ (1 / ε)) / ε) / y := ?_
  _ = 1 := this
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y)

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y) ≤
    ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y)
Tactic:
rw [setIntegral_congr (by simp)]
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y)
    (fun x_1 => (fun y => if y ∈ Ioc 0 1 then 1 else 0) x_1 * (Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1)) (Ioi 0)

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε) / ↑y)
    (fun x_1 => (fun y => if y ∈ Ioc 0 1 then 1 else 0) x_1 * (Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1)) (Ioi 0)
Tactic:
simp only [ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq, mem_Ioc]
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ EqOn (fun y => (if 0 < y ∧ y ≤ 1 then Ψ ((x / y) ^ (1 / ε)) / ε else 0) / y)
    (fun x_1 => if 0 < x_1 ∧ x_1 ≤ 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) (Ioi 0)

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ EqOn (fun y => (if 0 < y ∧ y ≤ 1 then Ψ ((x / y) ^ (1 / ε)) / ε else 0) / y)
    (fun x_1 => if 0 < x_1 ∧ x_1 ≤ 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) (Ioi 0)
Tactic:
intro y hy
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (if 0 < y ∧ y ≤ 1 then Ψ ((x / y) ^ (1 / ε)) / ε else 0) / y) y =
    (fun x_1 => if 0 < x_1 ∧ x_1 ≤ 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) y

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (if 0 < y ∧ y ≤ 1 then Ψ ((x / y) ^ (1 / ε)) / ε else 0) / y) y =
    (fun x_1 => if 0 < x_1 ∧ x_1 ≤ 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) y
Tactic:
aesop
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∫ (y : ℝ) in Ioi 0, (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y) ≤
    ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y
Tactic:
refine setIntegral_mono_on ?_ (integrable_of_integral_eq_one this) (by simp) ?_
State after:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ IntegrableOn (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y)) (Ioi 0) volume

case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ x_1 ∈ Ioi 0,
    (fun y => if y ∈ Ioc 0 1 then 1 else 0) x_1 * (Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1) ≤
      Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1

State before:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ IntegrableOn (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y * (Ψ ((x / y) ^ (1 / ε)) / ε / y)) (Ioi 0) volume
Tactic:
refine integrable_of_integral_eq_one this |>.bdd_mul ?_ (by use 1; aesop)
State after:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ AEStronglyMeasurable (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y) (volume.restrict (Ioi 0))

State before:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ AEStronglyMeasurable (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y) (volume.restrict (Ioi 0))
Tactic:
have : (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) = indicator (Ioc 0 1) (1 : ℝ → ℝ) := by
  aesop
State after:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this✝ : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
this : (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) = (Ioc 0 1).indicator 1
⊢ AEStronglyMeasurable (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y) (volume.restrict (Ioi 0))

State before:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this✝ : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
this : (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) = (Ioc 0 1).indicator 1
⊢ AEStronglyMeasurable (fun y => (fun y => if y ∈ Ioc 0 1 then 1 else 0) y) (volume.restrict (Ioi 0))
Tactic:
simp only [mem_Ioc, this, measurableSet_Ioc, aestronglyMeasurable_indicator_iff]
State after:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this✝ : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
this : (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) = (Ioc 0 1).indicator 1
⊢ AEStronglyMeasurable 1 ((volume.restrict (Ioi 0)).restrict (Ioc 0 1))

State before:
case calc_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this✝ : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
this : (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) = (Ioc 0 1).indicator 1
⊢ AEStronglyMeasurable 1 ((volume.restrict (Ioi 0)).restrict (Ioc 0 1))
Tactic:
exact aestronglyMeasurable_one
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∃ C, ∀ (x : ℝ), ‖(fun y => if y ∈ Ioc 0 1 then 1 else 0) x‖ ≤ C
Tactic:
use 1
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ (x : ℝ), ‖(fun y => if y ∈ Ioc 0 1 then 1 else 0) x‖ ≤ 1

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ (x : ℝ), ‖(fun y => if y ∈ Ioc 0 1 then 1 else 0) x‖ ≤ 1
Tactic:
aesop
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) = (Ioc 0 1).indicator 1
Tactic:
aesop
State after:
no goals

State before:
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ x_1 ∈ Ioi 0,
    (fun y => if y ∈ Ioc 0 1 then 1 else 0) x_1 * (Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1) ≤
      Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1
Tactic:
simp only [ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq]
State after:
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ x_1 ∈ Ioi 0, (if x_1 ∈ Ioc 0 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) ≤ Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1

State before:
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
⊢ ∀ x_1 ∈ Ioi 0, (if x_1 ∈ Ioc 0 1 then Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1 else 0) ≤ Ψ ((x / x_1) ^ (1 / ε)) / ε / x_1
Tactic:
intro y hy
State after:
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

State before:
case calc_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y
Tactic:
by_cases h : y ≤ 1
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y
Tactic:
aesop
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (if y ∈ Ioc 0 1 then Ψ ((x / y) ^ (1 / ε)) / ε / y else 0) ≤ Ψ ((x / y) ^ (1 / ε)) / ε / y
Tactic:
field_simp [mem_Ioc, h, and_false, reduceIte]
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε)) / (ε * y)

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε)) / (ε * y)
Tactic:
apply mul_nonneg
State after:
case neg.ha
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε))

case neg.hb
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ (ε * y)⁻¹

State before:
case neg.ha
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε))
Tactic:
apply Ψnonneg
State after:
case neg.ha.a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (x / y) ^ (1 / ε) > 0

State before:
case neg.ha.a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (x / y) ^ (1 / ε) > 0
Tactic:
exact rpow_pos_of_pos (div_pos xpos <| mem_Ioi.mp hy) _
State after:
no goals

State before:
case neg.hb
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ (ε * y)⁻¹
Tactic:
apply inv_nonneg.mpr <| mul_nonneg εpos.le (mem_Ioi.mp hy).le
State after:
no goals