awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
have obtain : ∀ (u : Set ι) (hu : u ∈ 𝓟 s) (v : Set α) (hv : v ∈ l) (huv : u ×ˢ v ⊆ t),
  IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
Tactic: obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
have refine : ∀ (x : α) (hx : x ∈ v), norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ C * μ.real s * ‖g x‖
Tactic: refine isBigO_iff.mpr ⟨C * μ.real s, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ C * μ.real s * ‖g x‖
have rw : norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ
Tactic: rw [mul_assoc, ← smul_eq_mul _ ‖g x‖, ← MeasureTheory.measureReal_restrict_apply_univ,
    ← integral_const, mul_comm, ← smul_eq_mul, ← integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ
have this : IsFiniteMeasure (μ.restrict s)
Tactic: haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rw [Measure.restrict_apply_univ s]; exact hμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ
have refine : (ae (μ.restrict s)).EventuallyLE (β := ℝ) (fun (a : ι) ↦ ‖f (a, x)‖) fun (x_1 : ι) ↦ ‖g x‖ • C
Tactic: refine (norm_integral_le_integral_norm _).trans <|
    integral_mono_of_nonneg (univ_mem' fun _ ↦ norm_nonneg _) (integrable_const _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) (fun (a : ι) ↦ ‖f (a, x)‖) fun (x_1 : ι) ↦ ‖g x‖ • C
have h : ∀ a ∈ s, ‖f (a, x)‖ ≤ ‖g x‖ • C
Tactic: filter_upwards [MeasureTheory.self_mem_ae_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ ‖g x‖ • C
have h : ‖f (y, x)‖ ≤ C * ‖g x‖
Tactic: rw [smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ Integrable f μ
have refine : StronglyMeasurableAtFilter f (cocompact α) μ
Tactic: refine integrable_iff_integrableAtFilter_cocompact.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ Integrable f μ
have refine_1 : StronglyMeasurableAtFilter f atBot μ
Tactic: refine integrable_iff_integrableAtFilter_atBot_atTop.mpr
    ⟨⟨ho.integrableAtFilter ?_ hg, ho'.integrableAtFilter ?_ hg'⟩, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
refine_1 : StronglyMeasurableAtFilter f atBot μ
⊢ Integrable f μ
have refine_2 : StronglyMeasurableAtFilter f atTop μ
Tactic: refine integrable_iff_integrableAtFilter_atBot_atTop.mpr
    ⟨⟨ho.integrableAtFilter ?_ hg, ho'.integrableAtFilter ?_ hg'⟩, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ IntegrableOn f (Iic a) μ
have refine : StronglyMeasurableAtFilter f atBot μ
Tactic: refine integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ
have refine : StronglyMeasurableAtFilter f atTop μ
Tactic: refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ Integrable f μ
have refine : StronglyMeasurableAtFilter f atBot μ
Tactic: refine integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_8 : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ
have refine : StronglyMeasurableAtFilter f atTop μ
Tactic: refine integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ
have h_int : IntegrableOn f (Ici 0) μ
Tactic: have h_int := (hf.locallyIntegrableOn (Ici 0)).integrableOn_of_isBigO_atTop ho hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Integrable f μ
have rw : IntegrableOn f (Iic 0) μ ∧ IntegrableOn f (Ici 0) μ
Tactic: rw [← integrableOn_univ, ← Iic_union_Ici_of_le le_rfl, integrableOn_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
rw : IntegrableOn f (Iic 0) μ ∧ IntegrableOn f (Ici 0) μ
⊢ Integrable f μ
have rw₁ : α
Tactic: rw [← integrableOn_univ, ← Iic_union_Ici_of_le le_rfl, integrableOn_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
| Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
have rhs : μ.restrict (Iic 0)
Tactic: rhs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
| μ.restrict (Iic 0)
have rw : Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))
Tactic: rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
| Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
have rw : Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))
Tactic: rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
have conv : Eq (α := Measure α) (Measure.map Neg.neg (μ.restrict (Ici 0))) (Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0)))
Tactic: conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ IntegrableOn f (Iic 0) μ
have h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
Tactic: have h_map_neg : (μ.restrict (Ici 0)).map Neg.neg = μ.restrict (Iic 0) := by
    conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ IntegrableOn f (Iic 0) μ
have rw : Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))
Tactic: rw [IntegrableOn, ← h_map_neg, measurableEmbedding_neg.integrable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))
have refine : AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))
Tactic: refine h_int.congr' ?_ hsymm.restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))
have refine : AEStronglyMeasurable (m₀ := inst_3) f (Measure.map Neg.neg (μ.restrict (Ici 0)))
Tactic: refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ⨍⁻ (_x : α), 0 ∂μ = 0
have rw : ∫⁻ (x : α), 0 ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = 0
Tactic: rw [laverage, lintegral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∫⁻ (x : α), 0 ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = 0
⊢ ⨍⁻ (_x : α), 0 ∂μ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [laverage, lintegral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
rw :
  ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ⨍⁻ (x : α), f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
rw :
  ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ⨍⁻ (x : α), f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₂ : HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), f x ∂μ)
Tactic: rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]