awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
hxK : x ∉ K
⊢ ‖g n x‖ * ‖f x‖ ≤ 0
have this₁ : g n x = 0
Tactic: have : g n x = 0 := by rw [← notMem_support, g_supp]; contrapose hxK; exact vK n hxK
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
⊢ Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))
have C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
Tactic: have C : ∀ n, ∀ᵐ x ∂μ, ‖g n x • f x‖ ≤ bound x := by
      intro n
      filter_upwards with x
      rw [norm_smul]
      refine le_indicator_apply (fun _ ↦ ?_) (fun hxK ↦ ?_)
      · have : ‖g n x‖ ≤ 1 := by
          have := g_range n (mem_range_self (f := g n) x)
          rw [Real.norm_of_nonneg this.1]
          exact this.2
        exact mul_le_of_le_one_left (norm_nonneg _) this
      · have : g n x = 0 := by rw [← notMem_support, g_supp]; contrapose hxK; exact vK n hxK
        simp [this]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
⊢ ∀ᵐ (x : M) ∂μ, Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
have h₁ : ∀ (x : M), Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
⊢ Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
have pos : ∀ (hxs : x ∈ s), Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
pos : ∀ (hxs : x ∈ s), Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
⊢ Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
have neg : ∀ (hxs : x ∉ s), Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∈ s
⊢ Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
have this₁ : ∀ (n : ℕ), g n x = 1
Tactic: have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
have neg : Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 0)
Tactic: simp_rw [indicator_of_notMem hxs f]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 0)
have neg : EventuallyEq.{0, u_2} (β := F) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ g n x • f x
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H_1 : Type u_3
inst_6 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H_1 M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H_1
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H_1
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
H : ∀ᶠ (n : ℕ) in atTop, g n x = 0
⊢ EventuallyEq.{0, u_2} (β := F) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ g n x • f x
have h₁ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x_2 : ℕ |
      Membership.mem (γ := Set ℕ) {x_3 : ℕ | (fun (n : ℕ) ↦ g n x = 0) x_3} x_2 →
        Membership.mem (γ := Set ℕ)
          {x_3 : ℕ |
            (fun (x_4 : ℕ) ↦ Eq.{u_2 + 1} (α := F) ((fun (x : ℕ) ↦ (0 : F)) x_4) ((fun (n : ℕ) ↦ g n x • f x) x_4)) x_3}
          x_2}
    a
Tactic: filter_upwards [H] with n hn using by simp [hn]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H_1 : Type u_3
inst_6 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H_1 M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H_1
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H_1
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
H : ∀ᶠ (n : ℕ) in atTop, g n x = 0
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_2 : ℕ |
        Membership.mem (γ := Set ℕ) {x_3 : ℕ | (fun (n : ℕ) ↦ g n x = 0) x_3} x_2 →
          Membership.mem (γ := Set ℕ)
            {x_3 : ℕ |
              (fun (x_4 : ℕ) ↦ Eq.{u_2 + 1} (α := F) ((fun (x : ℕ) ↦ (0 : F)) x_4) ((fun (n : ℕ) ↦ g n x • f x) x_4))
                x_3}
            x_2}
      a
⊢ EventuallyEq.{0, u_2} (β := F) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ g n x • f x
have h₂ : ∀ (a : ℕ), g a x = 0 → 0 = g a x • f x
Tactic: filter_upwards [H] with n hn using by simp [hn]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ EventuallyEq.{0, u_2} (β := F) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ g n x • f x
have neg : ∀ᶠ (n : ℕ) in atTop, g n x = 0
Tactic: suffices H : ∀ᶠ n in atTop, g n x = 0 by
          filter_upwards [H] with n hn using by simp [hn]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ ∃ (ε : ℝ), 0 < ε ∧ x ∉ thickening ε s
have hxs₁ : x ∉ ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s
Tactic: rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs
Cleared hypotheses: hxs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ ∀ᶠ (n : ℕ) in atTop, g n x = 0
have neg : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : x ∉ thickening ε s), ∀ᶠ (n : ℕ) in atTop, g n x = 0
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s := by
          rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs
          simpa using hxs