internlm/Lean-Github huggingface dataset:
Theorem: Smooth1LeOne_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, (Ψ (y ^ (1 / ε)) / ε) / y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, Ψ y / y := ?_
  _ = 1 := mass_one
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Theorem: Smooth1LeOne_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y
Tactic:
have := integral_comp_div_I0i_haar (fun y ↦ Ψ ((x / y) ^ (1 / ε)) / ε) xpos
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y
Theorem: Smooth1LeOne_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y
Tactic:
convert this.symm using 1
Proof state after:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Theorem: Smooth1LeOne_aux
Proof state before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
congr
Proof state after:
case h.e'_3.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ (fun y => Ψ (y ^ (1 / ε)) / ε / y) = fun y => (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Theorem: Smooth1LeOne_aux
Proof state before:
case h.e'_3.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
⊢ (fun y => Ψ (y ^ (1 / ε)) / ε / y) = fun y => (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
funext y
Proof state after:
case h.e'_3.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ Ψ (y ^ (1 / ε)) / ε / y = (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Theorem: Smooth1LeOne_aux
Proof state before:
case h.e'_3.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ Ψ (y ^ (1 / ε)) / ε / y = (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
congr
Proof state after:
case h.e'_3.e_f.h.e_a.e_a.e_a.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ y = x / (x / y)
Theorem: Smooth1LeOne_aux
Proof state before:
case h.e'_3.e_f.h.e_a.e_a.e_a.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ y = x / (x / y)
Tactic:
field_simp [mul_comm]
Proof state after:
no goals
Theorem: Smooth1LeOne_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Tactic:
have := integral_comp_rpow_I0i_haar_real (fun y ↦ Ψ y) (one_div_ne_zero εpos.ne')
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : ∫ (y : ℝ) in Ioi 0, |1 / ε| * (fun y => Ψ y) (y ^ (1 / ε)) / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ y) y / y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Theorem: Smooth1LeOne_aux
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this : ∫ (y : ℝ) in Ioi 0, |1 / ε| * (fun y => Ψ y) (y ^ (1 / ε)) / y = ∫ (y : ℝ) in Ioi 0, (fun y => Ψ y) y / y
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y
Tactic:
field_simp [ ← this, abs_of_pos <| one_div_pos.mpr εpos]
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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)]
Proof 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)
Theorem: Smooth1LeOne
Proof 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]
Proof 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)
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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) ?_
Proof 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
Theorem: Smooth1LeOne
Proof 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)
Proof 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))
Theorem: Smooth1LeOne
Proof 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
Proof 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))
Theorem: Smooth1LeOne
Proof 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]
Proof 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))
Theorem: Smooth1LeOne
Proof 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
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof 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]
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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
Proof 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
Theorem: Smooth1LeOne
Proof 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]
Proof 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)