mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
v : E
v_ne : v ≠ 0
hv₁ : x - v ∈ S
hv₂ : x + v ∈ S
⊢ x ∈ ∅

Tactic:
have key : x ∈ openSegment ℝ (x - v) (x + v) := mem_openSegment_sub_add _ _

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
v : E
v_ne : v ≠ 0
hv₁ : x - v ∈ S
hv₂ : x + v ∈ S
key : x ∈ openSegment ℝ (x - v) (x + v)
⊢ x ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsUniversal v
x : V
hx : G.Adj v x
⊢ False

Tactic:
simpa using

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsUniversal v
x : V
hx : G.Adj v x
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsIsolated v
x : V
hx : v ≠ x
⊢ Gᶜ.Adj v x

Tactic:
simpa using

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
v : V
h : G.IsIsolated v
x : V
hx : v ≠ x
⊢ ¬G.Adj v x
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsIsolated v
⊢ G.IsUniversal v

Tactic:
simpa using

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
h : Gᶜ.IsIsolated v
⊢ G.IsUniversal v
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p

Tactic:
simpa using

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ¬p₁ = p₃
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = (1 - 2⁻¹) * dist x z

Tactic:
← one_div,

Goal state after:
case hyz
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = (1 - 1 / 2) * dist x z
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, ‖p i -ᵥ p₀‖ ≤ r
⊢ p i -ᵥ p₀ ≠ p j -ᵥ p₀

Tactic:
simpa using

Goal state after:
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, ‖p i -ᵥ p₀‖ ≤ r
⊢ ¬p i = p j
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : 0 ≤ φ
⊢ ConvexOn ℝ s f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : 0 ≤ φ
⊢ ConvexOn ℝ s f
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : 0 ≤ φ
⊢ ConcaveOn ℝ s f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : 0 ≤ φ
⊢ ConcaveOn ℝ s f
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) + g (a • x + b • y) ≤
    a * f x + a * g x + (b * f y + b * g y) - (a * b * φ ‖x - y‖ + a * b * ψ ‖x - y‖)
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * f x + a * g x + (b * f y + b * g y) + (a * b * φ ‖x - y‖ + a * b * ψ ‖x - y‖) ≤
    f (a • x + b • y) + g (a • x + b • y)
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) + a * b * φ ‖x - y‖ ≤ a * f x + b * f y
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * b * φ ‖x + -y‖ ≤ f (a • x + b • y) + (-(a * f x) + -(b * f y))
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
⊢ False

Tactic:
have : 0 < 1 - ε := by linarith

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
⊢ False
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
⊢ s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)

Tactic:
simpa using

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
⊢ ¬j = i
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ s ∈ 𝓝 ((lineMap y x) 0)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
V : Type u_2
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ s ∈ 𝓝 y
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q : ℝ≥0∞
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fact (1 ≤ q)
inst✝³ : p.HolderConjugate q
inst✝² : NormedSpace ℝ G
inst✝¹ : SMulCommClass ℝ 𝕜 G
inst✝ : CompleteSpace G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ((lpPairing μ p q B) f) g = ∫ (x : α), (B (↑↑f x)) (↑↑g x) ∂μ

Tactic:
simpa using

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q : ℝ≥0∞
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : Fact (1 ≤ q)
inst✝³ : p.HolderConjugate q
inst✝² : NormedSpace ℝ G
inst✝¹ : SMulCommClass ℝ 𝕜 G
inst✝ : CompleteSpace G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ∫ (a : α), ↑↑(holder 1 B f g) a ∂μ = ∫ (x : α), (B (↑↑f x)) (↑↑g x) ∂μ
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide (s.points i)
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    w i < 0

Tactic:
s.sOppSide_affineSpan_faceOpposite_point_left_iff hw

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ w i < 0 ↔ w i < 0
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w)
      (s.points i) ↔
    w i < 0

Tactic:
by
  rw [sOppSide_comm, s.sOppSide_affineSpan_faceOpposite_point_left_iff hw]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
rw [rpow_neg]; positivity

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

Goal state before:
pp: r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0

Tactic:
simpa using

Goal state after:
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 0 ≤ r
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) y) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p ↦ ENNReal.ofReal (g p.2)
⊢ MeasurableSet {p | p.2 ∈ Ioc 0 (f p.1)}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) y) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p ↦ ENNReal.ofReal (g p.2)
⊢ MeasurableSet {p | p.2 ∈ Ioc 0 (f p.1)}
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
⊢ ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 s, g x ∂volume) ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
⊢ 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ 0 < ∫ (t : ℝ) in Ioc 0 s, g t ∂volume
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
a : α
ha : a ∈ {a | f a ≤ M}
⊢ a ∉ {a | M < f a}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
a : α
ha : a ∈ {a | f a ≤ M}
⊢ f a ≤ M
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ n ∈ Finset.range (N + 1)

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ n ≤ N
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F✝ : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
f : E → F✝
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
⊢ F =O[⊤] fun x ↦ (1 + ‖x‖) ^ k

Tactic:
simp_rw [F, isBigO_pi, Fin.forall_iff, Nat.lt_succ_iff]

Goal state after:
E : Type u_5
F✝ : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
f : E → F✝
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
⊢ ∀ (i : ℕ) (h : i ≤ n), (fun x ↦ iteratedFDeriv ℝ i f x) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case succ
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C' * (1 + ‖x‖) ^ k'

Tactic:
simpa using

Goal state after:
case succ
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ m (fun y ↦ fderiv ℝ f y) x‖ ≤ C' * (1 + ‖x‖) ^ k'
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ HasTemperateGrowth (fderiv ℝ fun x ↦ c)

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ HasTemperateGrowth 0
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ g x₀ * (1 + ‖x‖) ^ 0

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ g x₀