mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
H₁ : Integrable (g ∘ π * f) μ
⊢ AEStronglyMeasurable (automorphize (g ∘ π * f)) (Measure.map mk (μ.restrict 𝓕))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
⊢ ∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * automorphize f x ∂Measure.map mk (μ.restrict 𝓕)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ ∫ (x : G' ⧸ Γ'), automorphize (g ∘ π * f) x ∂Measure.map mk (μ'.restrict 𝓕') =
    ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
⊢ Integrable (g ∘ π * f) μ'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
H₁ : Integrable (g ∘ π * f) μ'
⊢ AEStronglyMeasurable (automorphize (g ∘ π * f)) (Measure.map mk (μ'.restrict 𝓕'))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
⊢ ∫ (x : G'), g ↑x * f x ∂μ' = ∫ (x : G' ⧸ Γ'), g x * automorphize f x ∂Measure.map mk (μ'.restrict 𝓕')

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ + ∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ ≤
    ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ (_t : ℝ) in Icc a b, δ ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hg : g = fun y ↦ f y - a - f' (y - x)
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
⊢ f = fun y ↦ a + f' (y - x) + g y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ (_t : ℝ) in Icc a b, δ ∂μ =
    (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ range (circleMap c R) = c +ᵥ R • range fun θ ↦ cexp (↑θ * I)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ (c +ᵥ R • range fun θ ↦ cexp (↑θ * I)) = sphere c |R|

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦
    ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R z : ℝ
hz : z ∈ univ
⊢ AnalyticAt ℝ (fun θ ↦ I) z

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ AnalyticOnNhd ℝ (circleMap c R) univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = 0 ↔ R = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ ↑‖deriv (circleMap c R) θ‖₊ ≤ ↑(Real.nnabs R)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ ↦ circleMap z R θ - w

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous fun θ ↦ (circleMap z R θ - w)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
a₀ b₀ : ℝ
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∫ (t : ℝ) in a₀..b₀, f x t ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
hR : R ≠ 0
⊢ map (circleMap c R) (codiscrete ℝ) ≤ codiscreteWithin (sphere c |R|)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: r x : ℝ
c : ℂ
⊢ circleMap c (-r) x = circleMap c r (x + π)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Tactic:
wlog hT : 0 < T
  · rcases (not_lt.1 hT).eq_or_lt with hT | hT
    · simp [hT]
    · rw [← neg_inj, ← integral_symm, ← integral_symm]
      simpa only [← sub_eq_add_neg, add_sub_cancel_right] using
        this hf.neg (t + T) (s + T) (neg_pos.mpr hT)
  simp only [integral_of_le, hT.le, le_add_iff_nonneg_right]
  have : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume :=
    ⟨fun c s _ => measure_preimage_add _ _ _⟩
  apply IsAddFundamentalDomain.setIntegral_eq (G := AddSubgroup.zmultiples T)
  exacts [isAddFundamentalDomain_Ioc hT t, isAddFundamentalDomain_Ioc hT s, hf.map_vadd_zmultiples]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
⊢ ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ (fun θ ↦ (∑ i ∈ s, f i) (circleMap c R θ)) = ∑ i ∈ s, fun θ ↦ f i (circleMap c R θ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∫ (x : ℝ) in 0..n • T, f x = n • ∫ (x : ℝ) in 0..T, f x
⊢ ∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ CircleIntegrable (∑ i ∈ s, f i) c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ a₀ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
m : ℕ
⊢ ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
⊢ CircleIntegrable (∑ᶠ (i : ι), f i) c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
𝕜 : Type u_3
F : Type u_4
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : ℂ → F
g : ℂ → 𝕜
hf : CircleIntegrable f c R
hg : ContinuousOn g (sphere c |R|)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
𝕜 : Type u_3
F : Type u_4
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : ℂ → 𝕜
g : ℂ → F
hf : CircleIntegrable f c R
hg : ContinuousOn g (sphere c |R|)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
a : ℝ
ha : a ∈ Iio x
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
𝕜 : Type u_3
inst✝ : NormedRing 𝕜
f g : ℂ → 𝕜
hf : CircleIntegrable f c R
hg : ContinuousOn g (sphere c |R|)
⊢ ContinuousOn (circleMap c R) [[0, 2 * π]]

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
a : ℝ
ha : a ∈ Ici a₀
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a₀

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = m • ∫ (x : ℝ) in 0..T, f x
n : ℕ
⊢ Int.negSucc n • T + (n + 1) • T = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
⊢ ∀ b ∈ Icc a₀ a, ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a₀, f x ∂μ - ∫ (x : ℝ) in a₀..b, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
⊢ CircleIntegrable f c 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ι 0 (2 * π)
⊢ (fun θ ↦ f (circleMap c (-R) θ)) x✝¹ = (fun θ ↦ (f ∘ circleMap c R) (θ + π)) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
⊢ CircleIntegrable f c (-R) ↔ CircleIntegrable f c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split : ∀ b ∈ Icc a₀ a, ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a₀, f x ∂μ - ∫ (x : ℝ) in a₀..b, f x ∂μ
⊢ IntervalIntegrable f μ (min a₀ a₀) (max a₀ a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ Ι 0 (2 * π) ⊆ univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ EqOn (fun θ ↦ f₁ (circleMap c R θ)) (fun θ ↦ f₂ (circleMap c R θ)) (circleMap c R ⁻¹' {z | f₁ z = f₂ z})

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ContinuousOn (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
⊢ CircleIntegrable f₂ c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y ↦ a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y ↦ a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y ↦ (fun y ↦ a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
⊢ ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
h₀ : ¬R = 0
h : IntegrableOn (fun θ ↦ (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume
θ : ℝ
⊢ circleMap 0 R θ * I ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
n : ℤ
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ a ≤ a₀

Tactic:
by

Goal state after: