internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
have := integral_comp_mul_right_Ioi (fun y ↦ f y / y) 0 ha
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (x : ℝ) in Ioi 0, (fun y => f y / ↑y) (x * a) = a⁻¹ • ∫ (x : ℝ) in Ioi (0 * a), (fun y => f y / ↑y) x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (x : ℝ) in Ioi 0, (fun y => f y / ↑y) (x * a) = a⁻¹ • ∫ (x : ℝ) in Ioi (0 * a), (fun y => f y / ↑y) x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
simp only [RCLike.ofReal_mul, zero_mul, eq_inv_smul_iff₀ (ne_of_gt ha)] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : a • ∫ (x : ℝ) in Ioi 0, f (x * a) / (↑x * ↑a) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : a • ∫ (x : ℝ) in Ioi 0, f (x * a) / (↑x * ↑a) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
rw [← integral_smul] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
rw [← this, setIntegral_congr (by simp)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ EqOn (fun y => f (y * a) / ↑y) (fun x => a • (f (x * a) / (↑x * ↑a))) (Ioi 0)
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ EqOn (fun y => f (y * a) / ↑y) (fun x => a • (f (x * a) / (↑x * ↑a))) (Ioi 0)
Tactic:
intro _ _
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ (fun y => f (y * a) / ↑y) x✝ = (fun x => a • (f (x * a) / (↑x * ↑a))) x✝
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ (fun y => f (y * a) / ↑y) x✝ = (fun x => a • (f (x * a) / (↑x * ↑a))) x✝
Tactic:
simp only [RCLike.real_smul_eq_coe_mul]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ f (x✝ * a) / ↑x✝ = ↑a * (f (x✝ * a) / (↑x✝ * ↑a))
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ f (x✝ * a) / ↑x✝ = ↑a * (f (x✝ * a) / (↑x✝ * ↑a))
Tactic:
rw [mul_comm (a : 𝕂), div_mul, mul_div_assoc, div_self ?_, mul_one]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ ↑a ≠ 0
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ ↑a ≠ 0
Tactic:
exact (RCLike.ofReal_ne_zero).mpr <| ne_of_gt ha
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_mul_right_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_mul_left_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a * y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
convert integral_comp_mul_right_I0i_haar f ha using 5
Proof state after:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ a * x✝ = x✝ * a
Theorem: MeasureTheory.integral_comp_mul_left_I0i_haar
Proof state before:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ a * x✝ = x✝ * a
Tactic:
ring
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
⊢ ∫ (y : ℝ) in Ioi 0, |p| * f (y ^ p) / y = ∫ (y : ℝ) in Ioi 0, f y / y
Tactic:
rw [← integral_comp_rpow_Ioi (fun y ↦ f y / y) hp, setIntegral_congr (by simp)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
⊢ EqOn (fun y => |p| * f (y ^ p) / y) (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) (Ioi 0)
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
⊢ EqOn (fun y => |p| * f (y ^ p) / y) (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) (Ioi 0)
Tactic:
intro y hy
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Tactic:
have ypos : 0 < y := mem_Ioi.mp hy
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Tactic:
field_simp [rpow_sub_one]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ |p| * f (y ^ p) * (y * y ^ p) = |p| * y ^ p * f (y ^ p) * y
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ |p| * f (y ^ p) * (y * y ^ p) = |p| * y ^ p * f (y ^ p) * y
Tactic:
ring
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_rpow_I0i_haar_real
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
have := integral_comp_rpow_Ioi (fun y ↦ f y / y) (p := -1) (by simp)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
rw [← this, setIntegral_congr (by simp)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ EqOn (fun y => f (1 / y) / ↑y) (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) (Ioi 0)
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ EqOn (fun y => f (1 / y) / ↑y) (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) (Ioi 0)
Tactic:
intro y hy
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Tactic:
have : (y : 𝕂) ≠ 0 := (RCLike.ofReal_ne_zero).mpr <| LT.lt.ne' hy
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Tactic:
field_simp [RCLike.real_smul_eq_coe_mul]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f (1 / y) = ↑(y ^ (-1 - 1)) * f (y ^ (-1)) * ↑y / ↑(y ^ (-1))
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f (1 / y) = ↑(y ^ (-1 - 1)) * f (y ^ (-1)) * ↑y / ↑(y ^ (-1))
Tactic:
ring_nf
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ (-2)) * f (y ^ (-1)) * ↑y * (↑(y ^ (-1)))⁻¹
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ (-2)) * f (y ^ (-1)) * ↑y * (↑(y ^ (-1)))⁻¹
Tactic:
rw [rpow_neg_one, mul_assoc, rpow_neg <| le_of_lt <| mem_Ioi.mp hy]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ 2)⁻¹ * f y⁻¹ * (↑y * (↑y⁻¹)⁻¹)
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ 2)⁻¹ * f y⁻¹ * (↑y * (↑y⁻¹)⁻¹)
Tactic:
field_simp [pow_two]
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
⊢ -1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_inv_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_div_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, f (a * y) / y := ?_
  _ = _ := integral_comp_mul_left_I0i_haar f ha
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (a * y) / ↑y
Theorem: MeasureTheory.integral_comp_div_I0i_haar
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (a / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (a * y) / ↑y
Tactic:
convert (integral_comp_inv_I0i_haar fun y ↦ f (a * (1 / y))).symm using 4
Proof state after:
case h.e'_2.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a / x✝) = f (a * (1 / x✝))

case h.e'_3.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a * x✝) = f (a * (1 / (1 / x✝)))
Theorem: MeasureTheory.integral_comp_div_I0i_haar
Proof state before:
case h.e'_2.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a / x✝) = f (a * (1 / x✝))
Tactic:
rw [mul_one_div]
Proof state after:
no goals
Theorem: MeasureTheory.integral_comp_div_I0i_haar
Proof state before:
case h.e'_3.h.e'_7.h.h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
x✝ : ℝ
⊢ f (a * x✝) = f (a * (1 / (1 / x✝)))
Tactic:
rw [one_div_one_div]
Proof state after:
no goals
Theorem: Complex.ofReal_rpow
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y
Tactic:
rw [rpow_def_of_pos h, ofReal_exp, ofReal_mul, Complex.ofReal_log h.le,
  Complex.cpow_def_of_ne_zero]
Proof state after:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑x ≠ 0
Theorem: Complex.ofReal_rpow
Proof state before:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
h : x > 0
y : ℝ
⊢ ↑x ≠ 0
Tactic:
simp only [ne_eq, ofReal_eq_zero, ne_of_gt h, not_false_eq_true]
Proof state after:
no goals
Theorem: Function.support_abs
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ (support fun x => ‖f x‖) = support f
Tactic:
simp only [support, ne_eq, mem_setOf_eq]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ {x | ¬‖f x‖ = 0} = {x | ¬f x = 0}
Theorem: Function.support_abs
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ {x | ¬‖f x‖ = 0} = {x | ¬f x = 0}
Tactic:
simp_rw [norm_ne_zero_iff]
Proof state after:
no goals
Theorem: Function.support_ofReal
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ (support fun x => ↑(f x)) = support f
Tactic:
apply Function.support_comp_eq (g := ofReal')
Proof state after:
case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
Theorem: Function.support_ofReal
Proof state before:
case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
Tactic:
simp [ofReal_zero]
Proof state after:
no goals
Theorem: Function.support_id
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (support fun x => x) = Iio 0 ∪ Ioi 0
Tactic:
ext x
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
⊢ (x ∈ support fun x => x) ↔ x ∈ Iio 0 ∪ Ioi 0
Theorem: Function.support_id
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
⊢ (x ∈ support fun x => x) ↔ x ∈ Iio 0 ∪ Ioi 0
Tactic:
simp only [mem_support, ne_eq, Iio_union_Ioi, mem_compl_iff, mem_singleton_iff]
Proof state after:
no goals
Theorem: Function.support_mul_subset_of_subset
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : Set ℝ
f g : ℝ → 𝕂
fSupp : support f ⊆ s
⊢ support (f * g) ⊆ s
Tactic:
simp_rw [support_mul', inter_subset, subset_union_of_subset_right fSupp]
Proof state after:
no goals
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
⊢ support f ⊆ s ×ˢ t
Tactic:
intro ⟨x, y⟩ hxy
Proof state after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y) ∈ s ×ˢ t
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y) ∈ s ×ˢ t
Tactic:
constructor
Proof state after:
case left
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ s

case right
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ t
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
case left
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ s
Tactic:
exact hx y (by simp only [Function.mem_support, ne_eq] at hxy ⊢; exact hxy)
Proof state after:
no goals
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).1 ∈ support fun x => f (x, y)
Tactic:
simp only [Function.mem_support, ne_eq] at hxy ⊢
Proof state after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
case right
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ t
Tactic:
exact hy x (by simp only [Function.mem_support, ne_eq] at hxy ⊢; exact hxy)
Proof state after:
no goals
Theorem: Function.support_of_along_fiber_subset_subset
Proof state before:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : (x, y) ∈ support f
⊢ (x, y).2 ∈ support fun y => f (x, y)
Tactic:
simp only [Function.mem_support, ne_eq] at hxy ⊢
Proof state after:
𝕂 : Type u_1
inst✝¹ : _root_.RCLike 𝕂
α : Type u_2
β : Type u_3
M : Type u_4
inst✝ : Zero M
f : α × β → M
s : Set α
t : Set β
hx : ∀ (y : β), (support fun x => f (x, y)) ⊆ s
hy : ∀ (x : α), (support fun y => f (x, y)) ⊆ t
x : α
y : β
hxy : ¬f (x, y) = 0
⊢ ¬f (x, y) = 0
Theorem: Function.support_deriv_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
⊢ support (deriv f) ⊆ Icc a b
Tactic:
have := support_deriv_subset (f := fun x ↦ f x)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ tsupport fun x => f x
⊢ support (deriv f) ⊆ Icc a b
Theorem: Function.support_deriv_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ tsupport fun x => f x
⊢ support (deriv f) ⊆ Icc a b
Tactic:
dsimp [tsupport] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
⊢ support (deriv f) ⊆ Icc a b
Theorem: Function.support_deriv_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
⊢ support (deriv f) ⊆ Icc a b
Tactic:
have := subset_trans this <| closure_mono fSupp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this✝ : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
this : support (deriv fun x => f x) ⊆ closure (Icc a b)
⊢ support (deriv f) ⊆ Icc a b
Theorem: Function.support_deriv_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this✝ : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
this : support (deriv fun x => f x) ⊆ closure (Icc a b)
⊢ support (deriv f) ⊆ Icc a b
Tactic:
rwa [closure_Icc] at this
Proof state after:
no goals