[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
have := I.locally_compact
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this : LocallyCompactSpace H
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
have := ChartedSpace.locallyCompact H M
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
have := I.secondCountableTopology
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : SecondCountableTopology H
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
have := ChartedSpace.secondCountable_of_sigma_compact H M
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
have := ManifoldWithCorners.metrizableSpace I M
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace M
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
let _ : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace M
x✝ : MetricSpace M := metrizableSpaceMetric M
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
[PROOFSTEP]
apply ae_eq_zero_of_forall_set_integral_isCompact_eq_zero' hf (fun s hs ↦ Eq.symm ?_)
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := hs.exists_isCompact_cthickening
[GOAL]
case intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 δ) ∧ Tendsto u atTop (𝓝 0) :=
  exists_seq_strictAnti_tendsto' δpos
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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)
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
let v : ℕ → Set M := fun n ↦ thickening (u n) s
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
obtain ⟨K, K_compact, vK⟩ : ∃ K, IsCompact K ∧ ∀ n, v n ⊆ K :=
  ⟨_, hδ, fun n ↦ thickening_subset_cthickening_of_le (u_pos n).2.le _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
have : ∀ n, ∃ (g : M → ℝ), support g = v n ∧ Smooth I 𝓘(ℝ) g ∧ Set.range g ⊆ Set.Icc 0 1 ∧ ∀ x ∈ s, g x = 1 :=
  by
  intro n
  rcases exists_msmooth_support_eq_eq_one_iff I isOpen_thickening hs.isClosed
      (self_subset_thickening (u_pos n).1 s) with
    ⟨g, g_smooth, g_range, g_supp, hg⟩
  exact ⟨g, g_supp, g_smooth, g_range, fun x hx ↦ (hg x).1 hx⟩
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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
⊢ ∀ (n : ℕ), ∃ g, support g = v n ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1 ∧ ∀ (x : M), x ∈ s → g x = 1
[PROOFSTEP]
intro n
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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
n : ℕ
⊢ ∃ g, support g = v n ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1 ∧ ∀ (x : M), x ∈ s → g x = 1
[PROOFSTEP]
rcases exists_msmooth_support_eq_eq_one_iff I isOpen_thickening hs.isClosed (self_subset_thickening (u_pos n).1 s) with
  ⟨g, g_smooth, g_range, g_supp, hg⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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
n : ℕ
g : M → ℝ
g_smooth : Smooth I 𝓘(ℝ, ℝ) g
g_range : range g ⊆ Icc 0 1
g_supp : support g = thickening (u n) s
hg : ∀ (x : M), x ∈ s ↔ g x = 1
⊢ ∃ g, support g = v n ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1 ∧ ∀ (x : M), x ∈ s → g x = 1
[PROOFSTEP]
exact ⟨g, g_supp, g_smooth, g_range, fun x hx ↦ (hg x).1 hx⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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
this : ∀ (n : ℕ), ∃ g, support g = v n ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1 ∧ ∀ (x : M), x ∈ s → g x = 1
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
choose g g_supp g_diff g_range hg using this
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
have L : Tendsto (fun n ↦ ∫ x, g n x • f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) :=
  by
  rw [← integral_indicator hs.measurableSet]
  let bound : M → ℝ := K.indicator (fun x ↦ ‖f x‖)
  have A : ∀ n, AEStronglyMeasurable (fun x ↦ g n x • f x) μ := fun n ↦
    (g_diff n).continuous.aestronglyMeasurable.smul hf.aestronglyMeasurable
  have B : Integrable bound μ := by
    rw [integrable_indicator_iff K_compact.measurableSet]
    exact (hf.integrableOn_isCompact K_compact).norm
  have C : ∀ n, ∀ᵐ x ∂μ, ‖g n x • f x‖ ≤ bound x := by
    intro n
    apply eventually_of_forall (fun 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 [← nmem_support, g_supp]; contrapose! hxK; exact vK n hxK
      simp [this]
  have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) :=
    by
    apply eventually_of_forall (fun x ↦ ?_)
    by_cases hxs : x ∈ s
    · have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
      simp [this, indicator_of_mem hxs f]
    · simp_rw [indicator_of_not_mem hxs f]
      apply tendsto_const_nhds.congr'
      suffices H : ∀ᶠ n in atTop, g n x = 0
      · filter_upwards [H] with n hn using by simp [hn]
      obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s :=
        by
        rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs 
        simpa using hxs
      filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
      rw [← nmem_support, g_supp]
      contrapose! hε
      exact thickening_mono hn.le s hε
  exact tendsto_integral_of_dominated_convergence bound A B C D
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
[PROOFSTEP]
rw [← integral_indicator hs.measurableSet]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
let bound : M → ℝ := K.indicator (fun x ↦ ‖f x‖)
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
have A : ∀ n, AEStronglyMeasurable (fun x ↦ g n x • f x) μ := fun n ↦
  (g_diff n).continuous.aestronglyMeasurable.smul hf.aestronglyMeasurable
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
have B : Integrable bound μ := by
  rw [integrable_indicator_iff K_compact.measurableSet]
  exact (hf.integrableOn_isCompact K_compact).norm
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
⊢ Integrable bound
[PROOFSTEP]
rw [integrable_indicator_iff K_compact.measurableSet]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
⊢ IntegrableOn (fun x => ‖f x‖) K
[PROOFSTEP]
exact (hf.integrableOn_isCompact K_compact).norm
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
have C : ∀ n, ∀ᵐ x ∂μ, ‖g n x • f x‖ ≤ bound x := by
  intro n
  apply eventually_of_forall (fun 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 [← nmem_support, g_supp]; contrapose! hxK; exact vK n hxK
    simp [this]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
⊢ ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
[PROOFSTEP]
intro n
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
⊢ ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
[PROOFSTEP]
apply eventually_of_forall (fun x ↦ ?_)
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
⊢ ‖g n x • f x‖ ≤ bound x
[PROOFSTEP]
rw [norm_smul]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
⊢ ‖g n x‖ * ‖f x‖ ≤ bound x
[PROOFSTEP]
refine le_indicator_apply (fun _ ↦ ?_) (fun hxK ↦ ?_)
[GOAL]
case refine_1
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
x✝ : x ∈ K
⊢ ‖g n x‖ * ‖f x‖ ≤ ‖f x‖
[PROOFSTEP]
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
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
x✝ : x ∈ K
⊢ ‖g n x‖ ≤ 1
[PROOFSTEP]
have := g_range n (mem_range_self (f := g n) x)
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
x✝ : x ∈ K
this : g n x ∈ Icc 0 1
⊢ ‖g n x‖ ≤ 1
[PROOFSTEP]
rw [Real.norm_of_nonneg this.1]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
x✝ : x ∈ K
this : g n x ∈ Icc 0 1
⊢ g n x ≤ 1
[PROOFSTEP]
exact this.2
[GOAL]
case refine_1
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
x✝ : x ∈ K
this : ‖g n x‖ ≤ 1
⊢ ‖g n x‖ * ‖f x‖ ≤ ‖f x‖
[PROOFSTEP]
exact mul_le_of_le_one_left (norm_nonneg _) this
[GOAL]
case refine_2
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
hxK : ¬x ∈ K
⊢ ‖g n x‖ * ‖f x‖ ≤ 0
[PROOFSTEP]
have : g n x = 0 := by rw [← nmem_support, g_supp]; contrapose! hxK; exact vK n hxK
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
hxK : ¬x ∈ K
⊢ g n x = 0
[PROOFSTEP]
rw [← nmem_support, g_supp]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
hxK : ¬x ∈ K
⊢ ¬x ∈ v n
[PROOFSTEP]
contrapose! hxK
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
hxK : x ∈ (fun n => thickening (u n) s) n
⊢ x ∈ K
[PROOFSTEP]
exact vK n hxK
[GOAL]
case refine_2
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
n : ℕ
x : M
hxK : ¬x ∈ K
this : g n x = 0
⊢ ‖g n x‖ * ‖f x‖ ≤ 0
[PROOFSTEP]
simp [this]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) :=
  by
  apply eventually_of_forall (fun x ↦ ?_)
  by_cases hxs : x ∈ s
  · have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
    simp [this, indicator_of_mem hxs f]
  · simp_rw [indicator_of_not_mem hxs f]
    apply tendsto_const_nhds.congr'
    suffices H : ∀ᶠ n in atTop, g n x = 0
    · filter_upwards [H] with n hn using by simp [hn]
    obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s :=
      by
      rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs 
      simpa using hxs
    filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
    rw [← nmem_support, g_supp]
    contrapose! hε
    exact thickening_mono hn.le s hε
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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 (𝓝 (indicator s f x))
[PROOFSTEP]
apply eventually_of_forall (fun x ↦ ?_)
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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 (𝓝 (indicator s f x))
[PROOFSTEP]
by_cases hxs : x ∈ s
[GOAL]
case pos
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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 (𝓝 (indicator s f x))
[PROOFSTEP]
have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
[GOAL]
case pos
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∈ s
this : ∀ (n : ℕ), g n x = 1
⊢ Tendsto (fun n => g n x • f x) atTop (𝓝 (indicator s f x))
[PROOFSTEP]
simp [this, indicator_of_mem hxs f]
[GOAL]
case neg
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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 (𝓝 (indicator s f x))
[PROOFSTEP]
simp_rw [indicator_of_not_mem hxs f]
[GOAL]
case neg
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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 (𝓝 0)
[PROOFSTEP]
apply tendsto_const_nhds.congr'
[GOAL]
case neg
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ s
⊢ (fun x => 0) =ᶠ[atTop] fun n => g n x • f x
[PROOFSTEP]
suffices H : ∀ᶠ n in atTop, g n x = 0
[GOAL]
case neg
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H✝ : Type u_3
inst✝⁷ : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H✝ M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H✝
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H✝
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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
⊢ (fun x => 0) =ᶠ[atTop] fun n => g n x • f x
[PROOFSTEP]
filter_upwards [H] with n hn using by simp [hn]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H✝ : Type u_3
inst✝⁷ : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H✝ M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H✝
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H✝
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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
n : ℕ
hn : g n x = 0
⊢ 0 = g n x • f x
[PROOFSTEP]
simp [hn]
[GOAL]
case H
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s :=
  by
  rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs 
  simpa using hxs
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => 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
[PROOFSTEP]
rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs 
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ s
⊢ ∃ ε, 0 < ε ∧ ¬x ∈ thickening ε s
[PROOFSTEP]
simpa using hxs
[GOAL]
case H.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ s
ε : ℝ
εpos : 0 < ε
hε : ¬x ∈ thickening ε s
⊢ ∀ᶠ (n : ℕ) in atTop, g n x = 0
[PROOFSTEP]
filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
[GOAL]
case h
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ s
ε : ℝ
εpos : 0 < ε
hε : ¬x ∈ thickening ε s
n : ℕ
hn : u n < ε
⊢ g n x = 0
[PROOFSTEP]
rw [← nmem_support, g_supp]
[GOAL]
case h
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ s
ε : ℝ
εpos : 0 < ε
hε : ¬x ∈ thickening ε s
n : ℕ
hn : u n < ε
⊢ ¬x ∈ v n
[PROOFSTEP]
contrapose! hε
[GOAL]
case h
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : ¬x ∈ s
ε : ℝ
εpos : 0 < ε
n : ℕ
hn : u n < ε
hε : x ∈ (fun n => thickening (u n) s) n
⊢ x ∈ thickening ε s
[PROOFSTEP]
exact thickening_mono hn.le s hε
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
bound : M → ℝ := indicator K fun x => ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x => g n x • f x) μ
B : Integrable bound
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
D : ∀ᵐ (x : M) ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (indicator s f x))
⊢ Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), indicator s (fun x => f x) x ∂μ))
[PROOFSTEP]
exact tendsto_integral_of_dominated_convergence bound A B C D
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
have : ∀ n, ∫ x, g n x • f x ∂μ = 0 := by
  refine' fun n ↦ h _ (g_diff n) _
  apply HasCompactSupport.of_support_subset_isCompact K_compact
  simpa [g_supp] using vK n
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
⊢ ∀ (n : ℕ), ∫ (x : M), g n x • f x ∂μ = 0
[PROOFSTEP]
refine' fun n ↦ h _ (g_diff n) _
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
n : ℕ
⊢ HasCompactSupport fun x => g n x
[PROOFSTEP]
apply HasCompactSupport.of_support_subset_isCompact K_compact
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
this : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
n : ℕ
⊢ (support fun x => g n x) ⊆ K
[PROOFSTEP]
simpa [g_supp] using vK n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝⁴ : LocallyCompactSpace H
this✝³ : LocallyCompactSpace M
this✝² : SecondCountableTopology H
this✝¹ : SecondCountableTopology M
this✝ : MetrizableSpace 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 : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ) (x : M), x ∈ s → g n x = 1
L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
this : ∀ (n : ℕ), ∫ (x : M), g n x • f x ∂μ = 0
⊢ 0 = ∫ (x : M) in s, f x ∂μ
[PROOFSTEP]
simpa [this] using L
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x
[PROOFSTEP]
have : ∀ᵐ x ∂μ, (f - f') x = 0 :=
  by
  apply ae_eq_zero_of_integral_smooth_smul_eq_zero I (hf.sub hf')
  intro g g_diff g_supp
  simp only [Pi.sub_apply, smul_sub]
  rw [integral_sub, sub_eq_zero]
  · exact h g g_diff g_supp
  · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
  · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
⊢ ∀ᵐ (x : M) ∂μ, (f - f') x = 0
[PROOFSTEP]
apply ae_eq_zero_of_integral_smooth_smul_eq_zero I (hf.sub hf')
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
⊢ ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • (f - f') x ∂μ = 0
[PROOFSTEP]
intro g g_diff g_supp
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
g : M → ℝ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_supp : HasCompactSupport g
⊢ ∫ (x : M), g x • (f - f') x ∂μ = 0
[PROOFSTEP]
simp only [Pi.sub_apply, smul_sub]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
g : M → ℝ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_supp : HasCompactSupport g
⊢ ∫ (x : M), g x • f x - g x • f' x ∂μ = 0
[PROOFSTEP]
rw [integral_sub, sub_eq_zero]
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
g : M → ℝ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_supp : HasCompactSupport g
⊢ ∫ (a : M), g a • f a ∂μ = ∫ (a : M), g a • f' a ∂μ
[PROOFSTEP]
exact h g g_diff g_supp
[GOAL]
case hf
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
g : M → ℝ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_supp : HasCompactSupport g
⊢ Integrable fun x => g x • f x
[PROOFSTEP]
exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
[GOAL]
case hg
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
g : M → ℝ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_supp : HasCompactSupport g
⊢ Integrable fun x => g x • f' x
[PROOFSTEP]
exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
[GOAL]
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : SmoothManifoldWithCorners I M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f f' : M → F
μ : Measure M
hf : LocallyIntegrable f
hf' : LocallyIntegrable f'
h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
x : M
hx : (f - f') x = 0
⊢ f x = f' x
[PROOFSTEP]
simpa [sub_eq_zero] using hx
