mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝[univ ×ˢ Icc 0 1] (s, 1)

Tactic:
nhdsWithin_prod_eq,

Goal state after:
case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝[univ] s ×ˢ 𝓝[Icc 0 1] 1
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 Ι b₀ s, ‖f p t‖ ∂μ + ∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ ≤
    ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ + ∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ

Tactic:
by
      gcongr
      · exact Eventually.of_forall (fun x ↦ norm_nonneg _)
      · exact (hf.uncurry_left _).norm.integrableOn_Icc
      · apply uIoc_subset_uIcc.trans (uIcc_subset_Icc ?_ ⟨hs.1.le, hs.2.le⟩ )
        simp [δpos.le]
      · exact Eventually.of_forall (fun x ↦ norm_nonneg _)
      · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
      · exact uIoc_subset_uIcc.trans (uIcc_subset_Icc ⟨a_lt.1.le, lt_b.1.le⟩ ⟨a_lt.2.le, lt_b.2.le⟩)

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

Goal state before:
pp: T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Goal state after:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(zmultiples T).op) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Goal state after:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
⊢ Continuous[instTopologicalSpaceProd, inst✝] fun st ↦ f st.1 (fract st.2)

Tactic:
by
  change Continuous (uncurry f ∘ Prod.map id fract)
  rw [continuous_iff_continuousAt]
  rintro ⟨s, t⟩
  rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)
  · rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]
    constructor
    · refine (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)
      · rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
        exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
      · simp [hf]
    · refine (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_) <;>
        simp [nhdsWithin_prod_eq, nhdsWithin_univ]
  · replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
    refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))
    exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := ⋯
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ I ⊆ Metric.closedBall 0 (|T| / 2)

Tactic:
simpa using

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ I ⊆ Icc (-(T / 2)) (T / 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case e'_4
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - (↑k - ↑n₁) * T)

Tactic:
simpa using

Goal state after:
case e'_4
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - (↑k - ↑n₁) * T)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
    Periodic f T → ∀ (t s : ℝ), 0 < T → ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
hT✝ : ¬0 < T
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = ∫ (x : ℝ) in s + T..s, f x

Tactic:
simpa using

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
    Periodic f T → ∀ (t s : ℝ), 0 < T → ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
hT✝ : ¬0 < T
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = ∫ (x : ℝ) in s + T..s, f x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case right
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
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a

Tactic:
simpa using

Goal state after:
case right
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
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a) a
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case neg.refine_1
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
H : ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0
⊢ AEStronglyMeasurable (fun θ ↦ f (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))

Tactic:
simpa using

Goal state after:
case neg.refine_1
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
H : ∀ {θ : ℝ}, circleMap 0 R θ * I ≠ 0
⊢ AEStronglyMeasurable (fun θ ↦ f (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
⊢ (fun x ↦ (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
      suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
        ((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE
          (deriv_circleMap_ne_zero hR)).eventually this
      filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
      simp_all [dist_eq, sub_eq_zero]

Goal state after:
case mp
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x ↦ (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 ↦ (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)

Tactic:
simpa using

Goal state after:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ ‖circleMap c R θ' - circleMap c R θ‖ ^ n
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀ ∩ Iic a) a

Tactic:
simpa using

Goal state after:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a) a
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
⊢ x ∈ Ioo 0 1

Tactic:
simpa using

Goal state after:
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
⊢ ¬f θ' = 0 ∧ ‖f θ'‖ < 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ MemLp f p (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ MemLp f p (ν Set.univ • μ)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ AEStronglyMeasurable f (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ AEStronglyMeasurable f (ν Set.univ • μ)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ MemLp f p (Measure.map Prod.snd (μ.prod ν))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ MemLp f p (μ Set.univ • ν)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ AEStronglyMeasurable f (Measure.map Prod.snd (μ.prod ν))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ AEStronglyMeasurable f (μ Set.univ • ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝¹ : TopologicalSpace X
f : β → X
inst✝ : SFinite ν
hf : AEStronglyMeasurable (fun x ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
⊢ AEStronglyMeasurable f ν

Tactic:
have := NeZero.mk hμ
  obtain ⟨y, hy⟩ := hf.prodMk_left.exists
  exact hy

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

Goal state before:
pp: case inr
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z ↦ (z - w) ^ n) c R

Tactic:
simpa using

Goal state after:
case inr
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ‖w - c‖ = |R|
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
R : Type u_4
inst✝² : NormedRing R
inst✝¹ : Module R E
inst✝ : IsBoundedSMul R E
f : α → R
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ ∀ (x : R) (y : E), ‖x • y‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
R : Type u_4
inst✝² : NormedRing R
inst✝¹ : Module R E
inst✝ : IsBoundedSMul R E
f : α → R
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ ∀ (x : R) (y : E), ‖x • y‖ ≤ ‖x‖ * ‖y‖
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))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
δ₁ : ℝ
δ₁0 : 0 < δ₁
hδ₁ : ∀ x_1 ∈ closedBall x δ₁ ∩ Box.Icc I, f x_1 ∈ closedBall (f x) (ε / 2 / 2)
δ : ℝ
hδ : δ ∈ Set.Ioc 0 δ₁
y₁ : Fin (n + 1) → ℝ
hy₁ : y₁ ∈ closedBall x δ ∩ Box.Icc I
y₂ : Fin (n + 1) → ℝ
hy₂ : y₂ ∈ closedBall x δ ∩ Box.Icc I
this : closedBall x δ ∩ Box.Icc I ⊆ closedBall x δ₁ ∩ Box.Icc I
⊢ dist (f y₁) (f y₂) ≤ ε / 2

Tactic:
calc
          dist (f y₁) (f y₂) ≤ dist (f y₁) (f x) + dist (f y₂) (f x) := dist_triangle_right _ _ _
          _ ≤ ε / 2 / 2 + ε / 2 / 2 := add_le_add (hδ₁ _ <| this hy₁) (hδ₁ _ <| this hy₂)
          _ = ε / 2 := add_halves _

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

Goal state before:
pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this : ContinuousWithinAt (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) 0 < ε / 2

Tactic:
simpa using

Goal state after:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this : ContinuousWithinAt (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ 0 < ε
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

Tactic:
simpa using

Goal state after:
case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t ↦ ‖f (circleMap c R t)‖ * (1 - ‖w‖ / R)⁻¹) volume 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖w / (circleMap c R θ - c)‖ < 1

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖w‖ / R < 1
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ eball 0 ↑R
⊢ ‖y✝‖ < ↑R

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ eball 0 ↑R
⊢ ‖y✝‖ < ↑R
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x ↦ 1) c R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)

Tactic:
simpa using

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x ↦ 1) c R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ Integrable (uncurry fun y x ↦ F x y) ((volume.restrict (uIoc c d)).prod (volume.restrict (uIoc a b)))

Tactic:
← integrable_swap_iff,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ Integrable ((uncurry fun y x ↦ F x y) ∘ Prod.swap) ((volume.restrict (uIoc a b)).prod (volume.restrict (uIoc c d)))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : β → E
⊢ ∫ (z : α × β), f z.2 ∂μ.prod ν = μ.real univ • ∫ (y : β), f y ∂ν

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : β → E
⊢ ∫ (z : α × β), f z.2 ∂μ.prod ν = μ.real univ • ∫ (y : β), f y ∂ν
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z ↦ I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x

Tactic:
simpa using

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z ↦ I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)