mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i = 0
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
simp only [mem_range, lt_self_iff_false, not_false_eq_true, sum_insert, coeff_natDegree,
    add_eq_zero_iff_eq_neg] at h

Goal state after:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : p.leadingCoeff * a ^ p.natDegree = -∑ i ∈ range p.natDegree, p.coeff i * a ^ i
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[n] α) ((next hf hx)^[n] β) ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
by
  rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective
    |>.dist_eq, ContinuousMap.dist_le]
  · intro t
    apply le_trans <| dist_iterate_next_apply_le hf hx α β n t
    gcongr
    exact abs_sub_le_max_sub t.2.1 t.2.2 _
  · have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
    positivity

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t

Tactic:
by
  apply HasDerivWithinAt.const_add
  have : Fact (t ∈ Icc tmin tmax) := ⟨ht⟩ -- needed to synthesise `FTCFilter` for `Icc`
  apply intervalIntegral.integral_hasDerivWithinAt_right _ -- need `CompleteSpace E` and `Icc`
    (continuousOn_comp hf hα hmem |>.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc t)
    (continuousOn_comp hf hα hmem _ ht)
  apply ContinuousOn.intervalIntegrable
  apply continuousOn_comp hf hα hmem |>.mono
  exact uIcc_subset_Icc ht₀ ht

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝¹ : Semiring R
inst✝ : FunLike F R ℝ
v : F
c : ℝ
⊢ gaussNorm v c 0 = 0

Tactic:
simp [gaussNorm]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
by
  have hroots' y (hy : (P.comp (-X)).IsRoot y) : y < -x := by
    grind [show P.IsRoot (-y) by rwa [IsRoot.def, eval_comp, eval_neg, eval_X, ← IsRoot.def] at hy]
  have hlc' : 0 ≤ Int.negOnePow (P.comp (-X)).natDegree * (P.comp (-X)).leadingCoeff := by
    rw [show (P.comp (-X)).leadingCoeff = P.leadingCoeff * Int.negOnePow P.natDegree by simp; ring,
      show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp], mul_comm, mul_assoc]
    simpa [Int.cast_negOnePow_natCast, pow_right_comm]
  cases P.natDegree.even_or_odd
  case inl h =>
    rw [Int.negOnePow_even] at hlc' ⊢
    · push_cast at hlc' ⊢; rw [one_mul] at hlc' ⊢
      have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
      simpa using this
    · simpa
    · simpa [natDegree_comp]
  case inr h =>
    rw [Int.negOnePow_odd] at hlc' ⊢
    · push_cast at hlc' ⊢; rw [neg_one_mul] at hlc' ⊢
      have := eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos hroots' (nonpos_of_neg_nonneg hlc')
      exact neg_pos.mpr (by simpa using this)
    · simpa
    · simpa [natDegree_comp]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
⊢ gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
by
  classical
  refine Real.iSup_le ?_ ?_
  · intro t
    obtain ⟨k, hk, hsum⟩ := IsNonarchimedean.finset_image_add vZero vNonneg vna
      (fun a ↦ coeff a.1 f * coeff a.2 g) (Finset.antidiagonal t)
    have hk' : k.1 + k.2 = t := by
      simpa [Finset.mem_antidiagonal] using hk (Finset.nonempty_def.mpr ⟨(t, 0), by simp⟩)
    have hprod : t.prod (c · ^ ·) = k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·) := by
      simp [← hk', Finsupp.prod_add_index' (h := (c · ^ ·)) (by grind) (by grind)]
    rw [hprod]
    refine (mul_le_mul hsum (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1) (c_prod_nonneg c hc k.2))
      (vNonneg _)).trans ?_
    have : v ((coeff k.1) f * (coeff k.2) g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) ≤
        (v (coeff k.1 f) * k.1.prod (c · ^ ·)) * (v (coeff k.2 g) * k.2.prod (c · ^ ·)) := by
      calc
      _ ≤ v (coeff k.1 f) * v (coeff k.2 g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) :=
        mul_le_mul (vMul _ _) (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1)
          (c_prod_nonneg c hc k.2)) (mul_nonneg (vNonneg _) (vNonneg _))
      _ = _ := by ring
    exact this.trans (mul_le_mul (le_gaussNorm v c f hbfd k.1) (le_gaussNorm v c g hbgd k.2)
      (mul_nonneg (vNonneg _) (c_prod_nonneg c hc k.2)) (gaussNorm_nonneg v c f vNonneg))
  · exact mul_nonneg (gaussNorm_nonneg v c f vNonneg) (gaussNorm_nonneg v c g vNonneg)

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ p.logMahlerMeasure = log ‖p.coeff 1‖ + log⁺ ‖(p.coeff 1)⁻¹ * p.coeff 0‖

Tactic:
by
  rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]
  simp [logMahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (circleAverage (fun x ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
rw [circleAverage_eq_intervalAverage]

Goal state after:
case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous fun x ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)

Tactic:
refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
⊢ (fun x1 x2 ↦ x1 < x2) = LiftRel fun x1 x2 ↦ x1 < x2

Tactic:
ext ⟨f⟩ ⟨g⟩

Goal state after:
case mk.mk
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : Preorder β
x✝¹ : (↑φ).Germ β
f : α → β
x✝ : (↑φ).Germ β
g : α → β
⊢ Quot.mk (⇑((↑φ).germSetoid β)) f < Quot.mk (⇑((↑φ).germSetoid β)) g ↔
    LiftRel (fun x1 x2 ↦ x1 < x2) (Quot.mk (⇑((↑φ).germSetoid β)) f) (Quot.mk (⇑((↑φ).germSetoid β)) g)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
⊢ 0 < 2 ^ (n + 2)

pp: n : ℕ
⊢ 0 < 2 ^ (n + 2)

Tactic:
all_goals apply pow_pos; norm_num

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = 0 / ↑1

Tactic:
zero_div

Goal state after:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = 0
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ 2 + ↑a / ↑b ≤ ↑c ^ 2 / ↑d ^ 2

Tactic:
add_div_eq_mul_add_div _ _ (ne_of_gt hb'),

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (2 * ↑b + ↑a) / ↑b ≤ ↑c ^ 2 / ↑d ^ 2
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n

Tactic:
zero_div

Goal state after:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
⊢ y ∈ Set.Icc 0 1 → y ∈ ofDigits '' Set.univ

Tactic:
hy

Goal state after:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
⊢ y ∈ ofDigits '' Set.univ
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
n p : ℕ
hp : Fact (Nat.Prime p)
hnpos : n > 0
y : ℤ
hm : y ^ n ≠ 0
hv : 0 ≠ 0
this : y ≠ 0
⊢ False

Tactic:
exact hv rfl

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
q : ℚ
hq : q < 0
⊢ ¬IsSquare q → True

Tactic:
implies_true

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r

Tactic:
simp [Infinitesimal, IsSt]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ cosh (arcosh x) = x

Tactic:
arcosh,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ cosh (log (x + √(x ^ 2 - 1))) = x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ sinh (arcosh x) = √(x ^ 2 - 1)

Tactic:
arcosh,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ sinh (log (x + √(x ^ 2 - 1))) = √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ arcosh (cosh x) = x

Tactic:
arcosh,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log (cosh x + √(cosh x ^ 2 - 1)) = x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - sqrt (x * y)) ≤ dist x y / 2

Tactic:
calc
    _ ≤ ((x + y) / 2 - x).toReal := by
      gcongr
      rw [le_sqrt_iff_sq_le, sq]
      gcongr
    _ = _ := by
      nth_rw 2 [← add_halves x]
      rw [add_div, add_tsub_add_eq_tsub_left, ← tsub_div, NNReal.coe_div, NNReal.coe_two, dist_comm,
        dist_eq, ← NNReal.coe_sub h, abs_eq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
y : ℝ
⊢ y ∈ Ioo (-1) 1 → x < y → (fun x ↦ (1 + x) / (1 - x)) x < (fun x ↦ (1 + x) / (1 - x)) y

Tactic:
hy

Goal state after:
x : ℝ
hx : x ∈ Ioo (-1) 1
y : ℝ
hy : y ∈ Ioo (-1) 1
⊢ x < y → (fun x ↦ (1 + x) / (1 - x)) x < (fun x ↦ (1 + x) / (1 - x)) y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y k : ℝ≥0
⊢ (k * x).agm (k * y) = k * x.agm y

Tactic:
agm,

Goal state after:
x y k : ℝ≥0
⊢ ⨅ n, ((k * x).agmSequences (k * y) n).2 = k * ⨅ n, (x.agmSequences y n).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ qaryEntropy q 0 = 0

Tactic:
simp [qaryEntropy]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ qaryEntropy q 1 = log ↑(↑q - 1)

Tactic:
simp [qaryEntropy]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: x✝ : ℝ
⊢ qaryEntropy 2 x✝ = binEntropy x✝

Tactic:
simp [qaryEntropy]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Tactic:
exact natDegree_mul_le.trans (by simp [add_comm 2, cosPoly_natDegree_le n])

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

Goal state before:
pp: p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
cases eq_or_lt_of_le' ht with
  | inl ht_zero => simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]
  | inr ht_pos =>
    refine mul_nonneg (by positivity) ?_
    rw [sub_nonneg]
    gcongr
    linarith

Goal state after:
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 : ℝ
⊢ y ∈ Ici 0 → x ≤ y → p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
hy

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
⊢ x ≤ y → p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
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 [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ 2 * (2 * ↑π) ^ (-1) * Gamma 1 = 1 / ↑π

Tactic:
cpow_neg_one,

Goal state after:
⊢ 2 * (2 * ↑π)⁻¹ * Gamma 1 = 1 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * (↑π ^ (-1) * 1)⁻¹

Tactic:
cpow_neg_one,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * ((↑π)⁻¹ * 1)⁻¹
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ

Tactic:
have maxr_nonneg : 0 ≤ maxr :=
    le_csSup_of_le (b := 0) (IsCompact.bddAbove (quasispectrum.isCompact _)) (by simp) le_rfl

Goal state after:
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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
⊢ IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Ioi 0) μ ∧
    a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x ↦ (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ -(2 * ((2 * ↑π) ^ (-1) * log (2 * ↑π))) = -log (2 * ↑π) / ↑π

Tactic:
cpow_neg_one,

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x ↦ (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ -(2 * ((2 * ↑π)⁻¹ * log (2 * ↑π))) = -log (2 * ↑π) / ↑π
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-log (2 * ↑π) / ↑π + 2 * (2 * ↑π) ^ (-1) * -↑γ) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
cpow_neg_one,

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-log (2 * ↑π) / ↑π + 2 * (2 * ↑π)⁻¹ * -↑γ) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ rexp (-y) * |1 - 2 * y| ≤ 1

Tactic:
have hynonneg : 0 ≤ y := by
    rw [hy, mul_assoc]
    exact mul_nonneg hε.le (mul_self_nonneg x)

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ rexp (-y) * |1 - 2 * y| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℝ
h : b = -1 ∨ b = 0 ∨ b = 1
⊢ logb b =O[⊤] log

Tactic:
obtain rfl | rfl | rfl := h
    all_goals simpa [-Asymptotics.isBigO_top] using! Asymptotics.isBigO_zero log ⊤

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
choose htu hto _ using ht

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε
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
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ‖f‖ - liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), f x ∂μ
this : limsup (fun i ↦ ‖f‖ - ∫ (x : X), f x ∂μs i) L = ‖f‖ - liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
_root_.sub_le_sub_iff_left ‖f‖

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
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
this : limsup (fun i ↦ ‖f‖ - ∫ (x : X), f x ∂μs i) L = ‖f‖ - liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
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 →ᵇ ℝ
⊢ Tendsto (fun i ↦ ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))

Tactic:
rcases eq_or_neBot L with rfl | hL
  · simp only [tendsto_bot]
  have obs := BoundedContinuousFunction.isBounded_range_integral μs f
  have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
  have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
  apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)
  · have key := h _ (f.add_norm_nonneg)
    simp_rw [f.integral_add_const ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
    rwa [this, add_le_add_iff_right] at key
  · have key := h _ (f.norm_sub_nonneg)
    simp_rw [f.integral_const_sub ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := liminf_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
    rwa [this, sub_le_sub_iff_left] at key
  · exact bdd_above
  · exact bdd_below

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
y : ℝ
⊢ y ∈ Ioc 0 ↑x → 0 y ≤ y ^ n

Tactic:
hy

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
y : ℝ
hy : y ∈ Ioc 0 ↑x
⊢ 0 y ≤ y ^ n