mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
h_lim :
  {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2} ∈ 𝓝[>] 0
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
mem_nhdsWithin_iff

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
h_lim :
  ∃ ε_1 > 0,
    ball 0 ε_1 ∩ Ioi 0 ⊆
      {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2}
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ x ^ (p - 1) * x = x ^ p

Tactic:
simpa using

Goal state after:
case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ x ^ (p - 1) * x = x ^ p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
simpa using

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : x = 0
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + y)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (Ioi 0 ×ˢ s)

Tactic:
let g : ℝ × ℝ → ℝ := fun q => q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
  refine ContinuousOn.congr (f := g) ?_ fun q => ?_
  · simp only [g]
    refine ContinuousOn.mul ?_ ?_
    · refine ContinuousOn.mul ?_ (by fun_prop)
      exact ContinuousOn.rpow_const (by fun_prop) (by grind)
    · exact ContinuousOn.inv₀ (by fun_prop) (by grind)
  · intro hq
    simp [Function.uncurry, g, rpowIntegrand₀₁_eq_pow_div hp (le_of_lt hq.1) (hs hq.2)]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
simpa using

Goal state after:
this : Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hff'
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ∀ x_1 ∈ Ioi 0, HasDerivWithinAt (fun x_2 ↦ x * x_2) x (Ioi x_1) x_1

Tactic:
simpa using

Goal state after:
case hff'
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ∀ (x_1 : ℝ), 0 < x_1 → HasDerivWithinAt (fun x_2 ↦ x * x_2) x (Ici x_1) x_1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hg_cont
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ioi 0)

Tactic:
simpa using

Goal state after:
case hg_cont
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hg1
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ici 0) volume

Tactic:
simpa using

Goal state after:
case hg1
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ici 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ s ≠ 0

Tactic:
simpa using

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ¬s = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
          refine ContinuousOn.mono ?_ hspec
          have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
          fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
by
  have hspec : quasispectrum ℝ a ⊆ Ici 0 := by grind
  have h_mapsTo : MapsTo (t⁻¹ • · : ℝ → ℝ) (Ici 0) (Ici 0) := by
    intro x hx
    simp only [mem_Ici, smul_eq_mul] at hx ⊢
    positivity
  calc _ = cfcₙ (fun x => t ^ ((p : ℝ) - 1) * (rpowIntegrand₀₁ p 1 (t⁻¹ • x))) a := by
          refine cfcₙ_congr ?_
          refine Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (fun x => rpowIntegrand₀₁ p 1 (t⁻¹ • x)) a := by
          refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_
          refine ContinuousOn.mono ?_ hspec
          have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
          fun_prop
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
          congr! 1
          refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_
          exact continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <|
            (h_mapsTo.mono_left hspec).image_subset

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gamma (-γ) 1

Tactic:
simpa using

Goal state after:
⊢ HasDerivAt Gamma (-γ) 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ rexp (-x)
⊢ (fun x ↦ rexp (-x)) =o[atTop] fun x ↦ x ^ s

Tactic:
simpa using

Goal state after:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ rexp (-x)
⊢ (fun x ↦ rexp (-x)) =o[atTop] fun x ↦ x ^ s
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gamma (-↑γ) 1

Tactic:
simpa using

Goal state after:
⊢ HasDerivAt Gamma (-↑γ) 1
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_2
this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)
⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

Tactic:
simpa using

Goal state after:
case refine_2
this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)
⊢ HasDerivAt Gamma (-(↑√π * (↑γ + 2 * log 2))) 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)

Tactic:
simpa using

Goal state after:
a : ℂ
ha : 0 < a.re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ ∑' (n : ℤ), rexp (-π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-π / a * ↑n ^ 2)

Tactic:
simpa using

Goal state after:
a : ℝ
ha : 0 < a
⊢ ∑' (a_1 : ℤ), cexp (-↑π * ↑a * ↑a_1 ^ 2) = 1 / ↑a ^ (1 / 2) * ∑' (a_1 : ℤ), cexp (-↑π / ↑a * ↑a_1 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
by
  rw [← not_lt, logb_pos_iff hb hx, not_lt]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a) ≤ t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • b)

Tactic:
gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ rexp (-1) < x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ∈ interior (Ici (rexp (-1)))
⊢ rexp (-1) < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb

Goal state after:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌊logb (↑b) r⌋ = Int.log b r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb

Goal state after:
case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ edist 0 f

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ edist 0 f
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ Tendsto (fun x ↦ logb b x ^ n / id x) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
b : ℝ
n : ℕ
⊢ Tendsto (fun x ↦ logb b x ^ n / x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log

Tactic:
simpa using

Goal state after:
case inl
⊢ (fun x ↦ 0) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (x * c)) =O[atTop] log

Tactic:
simpa using

Goal state after:
c : ℝ
⊢ (fun x ↦ log (c * x)) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
⊢ (fun x ↦ logb b (c * x)) =O[atTop] log

Tactic:
simpa using

Goal state after:
b c : ℝ
⊢ (fun x ↦ (log b)⁻¹ * log (c * x)) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b c : ℝ
⊢ (fun x ↦ logb b (x * c)) =O[atTop] log

Tactic:
simpa using

Goal state after:
b c : ℝ
⊢ (fun x ↦ logb b (c * x)) =O[atTop] log
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ (IsCompact ∘ closure) (closure K)

Tactic:
simpa using

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ IsCompact (closure K)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case zero
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
⊢ ∀ x ∈ Ico x₀ (r ^ (0 + 1) * x₀), P x

Tactic:
simpa using

Goal state after:
case zero
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
⊢ ∀ (x : ℝ), x₀ ≤ x → x < r * x₀ → P x
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (?m.103 '' Set.univ)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (Set.range ?m.103)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ BddBelow (?m.125 '' Set.univ)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ BddBelow (Set.range ?m.125)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (?m.103 '' Set.univ)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
⊢ BddAbove (Set.range ?m.103)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ BddBelow (?m.125 '' Set.univ)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ BddBelow (Set.range ?m.125)
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ Polynomial.eval (↑n - 1) (descPochhammer ℝ n) = 0

Tactic:
simpa using

Goal state after:
n : ℕ
hn : 0 < n
⊢ Polynomial.eval (↑(n - 1)) (descPochhammer ℝ n) = 0
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun x_1 ↦ ((1 + (↑x_1)⁻¹ • -(ε • g * g)) ^ x_1) x) atTop (𝓝 (rexp (-(ε * g x * g x))))

Tactic:
simpa using

Goal state after:
case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun x_1 ↦ (1 + -(ε * (g x * g x)) / ↑x_1) ^ x_1) atTop (𝓝 (rexp (-(ε * (g x * g x)))))
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
f : ℝ → ℝ := (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
h_jensen : f (∑ i ∈ t, w i • ↑(p i)) ≤ ∑ i ∈ t, w i • f ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)

Tactic:
simpa using

Goal state after:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
f : ℝ → ℝ := (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0
h_jensen : f (∑ i ∈ t, w i • ↑(p i)) ≤ ∑ i ∈ t, w i • f ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) ≤ ∑ i ∈ t, w i * ↑((p i).descFactorial n)
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤
    (∑ i ∈ t, w i * Polynomial.eval (↑(p i)) (descPochhammer ℝ n)) / ↑n.factorial

Tactic:
descPochhammer_eval_eq_descFactorial

Goal state after:
n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤
    (∑ x ∈ t, w x * ↑((p x).descFactorial n)) / ↑n.factorial
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
have hgA : g ∈ A := hg'A.choose_spec.1

Goal state after:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.ω₁ / 2 ∉ L.lattice

Tactic:
simpa using

Goal state after:
L : PeriodPair
⊢ L.ω₁ / 2 ∉ L.lattice