-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos
    [MetrizableSpace α] [IsLocallyFiniteMeasure μ] (hs : IsCompact s)
    (hμ : ∀ u, IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)) {c : α → ℝ} (hc : ContinuousOn c s)
    (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ s)
    (hmg : IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) :
    Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ)
      atTop (𝓝 (g x₀))

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
n : ℕ
x : α
hx : x ∈ s
⊢ 0 ≤ φ n x

Tactic:
apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)

Result:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
n : ℕ
x : α
hx : x ∈ s
⊢ 0 ≤ ∫ (x : α) in s, c x ^ n ∂μ

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * (μ (v ∩ s)).toReal ≤ ∫ (y : α) in s, c y ^ n ∂μ
⊢ c x ^ n / ∫ (x : α) in s, c x ^ n ∂μ ≤ t ^ n / (t' ^ n * (μ (v ∩ s)).toReal)

Tactic:
have := ENNReal.toReal_pos (hμ v v_open x₀_v).ne'
  ((measure_mono inter_subset_right).trans_lt hs.measure_lt_top).ne

Result:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * (μ (v ∩ s)).toReal ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < (μ (v ∩ s)).toReal
⊢ c x ^ n / ∫ (x : α) in s, c x ^ n ∂μ ≤ t ^ n / (t' ^ n * (μ (v ∩ s)).toReal)

Proof state:
case inr.intro.intro
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
⊢ ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t

Tactic:
refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩

Result:
case inr.intro.intro
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
⊢ x ≠ x₀

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ (v ∩ s)).toReal⁻¹ * (t / t') ^ n
⊢ t / t' < 1

Tactic:
exact (div_lt_one t'_pos).2 tt'

Result:
no goals