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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b : B
a : A
⊢ (a ∈ Function.support fun a ↦ f (b * φ a)) → ∀ ⦃y : A⦄, (y ∈ Function.support fun a ↦ f (b * φ a)) → a = y

Tactic:
ha

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h :
  μC Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b : B
a : A
ha : a ∈ Function.support fun a ↦ f (b * φ a)
⊢ ∀ ⦃y : A⦄, (y ∈ Function.support fun a ↦ f (b * φ a)) → a = y
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ -(↑C * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), g x ∂↑μ

pp: case refine_2
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), g x ∂↑μ ≤ ↑C * ‖g.toBoundedContinuousFunction‖

Tactic:
· calc - (C * ‖g.toBoundedContinuousFunction‖)
      _ ≤ ∫ (x : E), - ‖g.toBoundedContinuousFunction‖ ∂μ := by
        simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
        gcongr
        exact hμ
      _ ≤ ∫ x, g x ∂μ := by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Goal state after:
case refine_2
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), g x ∂↑μ ≤ ↑C * ‖g.toBoundedContinuousFunction‖
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁.hf
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val '' s)

pp: case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)

Tactic:
· exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Goal state after:
case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
⊢ ∀ x ∈ range ⇑φ, ∀ u ∈ tangentConeAt ℝ (range ⇑φ) x, ∀ v ∈ tangentConeAt ℝ (range ⇑φ) x, ((dω x) u) v = ((dω x) v) u

Tactic:
intro x hx u hu v hv

Goal state after:
case refine_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
hφs : range ⇑φ ⊆ s
x : E
hx : x ∈ range ⇑φ
u : E
hu : u ∈ tangentConeAt ℝ (range ⇑φ) x
v : E
hv : v ∈ tangentConeAt ℝ (range ⇑φ) x
⊢ ((dω x) u) v = ((dω x) v) u
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case hω
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
⊢ a ∈ s → HasFDerivWithinAt (fun a ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a)) (?m.54 a) s a

Tactic:
ha

Goal state after:
case hω
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
⊢ HasFDerivWithinAt (fun a ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a)) (?m.54 a) s a
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝³ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
y : E
this : ProperSpace E
hy : ¬y = 0
h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0)
r : ℝ
h_le : ∀ (μ : Measure E), μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ μ {x | r * ‖y‖⁻¹ < ‖x‖}
μ : Measure E
hμS : μ ∈ S
⊢ μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ ⨆ (_ : μ ∈ S), μ {x | r * ‖y‖⁻¹ < ‖x‖}

Tactic:
by simp [hμS, h_le]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε

Tactic:
intro f f_disj f_meas hf ε εpos
    rcases ENNReal.exists_pos_sum_of_countable' (ENNReal.half_pos εpos.ne').ne' ℕ with ⟨δ, δpos, hδ⟩
    have A i : ∃ t ∈ C, μ (t ∆ (f i)) < δ i := hf i _ (δpos i)
    choose! t tC ht using A
    have : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0) :=
      tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
        (fun i ↦ (f_meas i).nullMeasurableSet) f_disj
    obtain ⟨n, hn⟩ : ∃ n, μ (⋃ i ∈ Ici n, f i) < ε / 2 :=
      ((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists
    refine ⟨⋃ i ∈ Finset.range n, t i, hC.biUnion_mem _ (fun i hi ↦ tC _), ?_⟩
    calc μ ((⋃ i ∈ Finset.range n, t i) ∆ (⋃ i, f i))
    _ ≤ μ ((⋃ i ∈ Finset.range n, (t i) ∆ (f i)) ∪ ⋃ i ∈ Ici n, f i) := by
      gcongr
      intro x hx
      simp only [Finset.mem_range, mem_symmDiff, mem_iUnion, exists_prop, not_exists, not_and,
        mem_Ici, mem_union] at hx ⊢
      grind
    _ ≤ ∑ i ∈ Finset.range n, μ (t i ∆ f i) + μ (⋃ i ∈ Ici n, f i) := by
      apply (measure_union_le _ _).trans
      gcongr
      apply measure_biUnion_finset_le
    _ ≤ ∑ i ∈ Finset.range n, δ i + μ (⋃ i ∈ Ici n, f i) := by
      gcongr with i; exact (ht i).le
    _ ≤ ∑' i, δ i + μ (⋃ i ∈ Ici n, f i) := by
      gcongr; exact ENNReal.sum_le_tsum (Finset.range n)
    _ < ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves ε

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case inl.inl.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 0
h✝¹ : μ t = 0
h✝ : μ (s ∩ t) = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inl.inl.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 0
h✝¹ : μ t = 0
h✝ : μ (s ∩ t) = 1
⊢ μ (s ∩ t) = μ s * μ t

pp: case inl.inr.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 0
h✝¹ : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inl.inr.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 0
h✝¹ : μ t = 1
h✝ : μ (s ∩ t) = 1
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inl.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 1
h✝¹ : μ t = 0
h✝ : μ (s ∩ t) = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inl.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 1
h✝¹ : μ t = 0
h✝ : μ (s ∩ t) = 1
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inr.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 1
h✝¹ : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ μ (s ∩ t) = μ s * μ t

pp: case inr.inr.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝² : μ s = 1
h✝¹ : μ t = 1
h✝ : μ (s ∩ t) = 1
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
all_goals try simp_all [measure_inter_eq_one]

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

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
hs : s ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet s

Tactic:
· rw [← hgen]
      exact generateFrom_mono <| le_trans self_subset_generateSetAlgebra <|
        generateSetAlgebra_mono <| subset_union_left ..

Goal state after:
case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
hs : s ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case basic
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
s u : Set α
hu : u ∈ C
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯).IsCaratheodory u

Tactic:
| basic u hu =>

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
m : Measure X
hs : MeasurableSet s
h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E
i : Finpartition ⟨s, ⋯⟩
a : Subtype MeasurableSet
⊢ a ∈ ↑i.parts → ∀ ⦃y : Subtype MeasurableSet⦄, y ∈ ↑i.parts → a ≠ y → Function.onFun Disjoint Subtype.val a y

Tactic:
ha

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
m : Measure X
hs : MeasurableSet s
h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E
i : Finpartition ⟨s, ⋯⟩
a : Subtype MeasurableSet
ha : a ∈ ↑i.parts
⊢ ∀ ⦃y : Subtype MeasurableSet⦄, y ∈ ↑i.parts → a ≠ y → Function.onFun Disjoint Subtype.val a y
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.Integrable f
⊢ ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
rw [← setIntegral_add_compl (μ := μ) hs hfi, add_sub_cancel_left]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a
u_lim : Tendsto u atTop (𝓝 a)
⊢ hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
replace u_lt_a n : u n < a := (u_lt_a n).2

Goal state after:
case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
⊢ hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
x : α
hx : a ≤ x
⊢ x ∈ ⋃ n, Icc a (u n)

Tactic:
simpa [hx] using (hu.eventually (Ici_mem_atTop x)).exists

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
hst : s ⊆ t
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
apply (measure_mono hst).trans

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
hst : s ⊆ t
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation t ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case neg
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
m'' : VectorMeasure α E := of_additive_of_le_measure m' ⋯ ⋯ ⋯
s : Set α
hs : ¬MeasurableSet s
⊢ ‖m' s‖ₑ ≤ μ s

Tactic:
· simp [m', hs]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ ‖m₀ s‖ₑ ≤ μ (P.parts.sup id)

Tactic:
rw [hm₀, AddContent.supClosure_apply_finpartition hC _ PC, Finset.sup_set_eq_biUnion,
      measure_biUnion_finset P.disjoint (fun b hb ↦ hCmeas _ (PC hb))]

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ ‖∑ s ∈ P.parts, m s‖ₑ ≤ ∑ p ∈ P.parts, μ (id p)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
A : ∀ s ∈ supClosure C, ‖m₀ s‖ₑ ≤ μ s
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
have B (s) (hs : s ∈ supClosure C) : MeasurableSet s := by
    rw [hC.mem_supClosure_iff] at hs
    rcases hs with ⟨P, PC⟩
    rw [← P.sup_parts, Finset.sup_set_eq_biUnion]
    exact Finset.measurableSet_biUnion _ (fun b hb ↦ hCmeas _ (PC hb))

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
A : ∀ s ∈ supClosure C, ‖m₀ s‖ₑ ≤ μ s
B : ∀ s ∈ supClosure C, MeasurableSet s
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : μ.HasProd ν B
⊢ ∃ ρ, ∀ (s : Set Y) (t : Set X), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B.flip (ν s)) (μ t)

Tactic:
by
    refine ⟨(μ.prod ν B).map Prod.swap, fun s t hs ht ↦ ?_⟩
    rw [map_apply _ (by fun_prop) (hs.prod ht)]
    simp

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
⊢ μ.totalVariation = VectorMeasure.variation μ

Tactic:
by
  ext r hr
  apply le_antisymm
  · obtain ⟨s, hs, hpos, hneg, hposPart, hnegPart⟩ := μ.toJordanDecomposition_spec
    calc μ.totalVariation r
      _ = ‖μ (s ∩ r)‖ₑ + ‖μ (sᶜ ∩ r)‖ₑ := by
          rw [totalVariation, Measure.add_apply, hposPart, hnegPart,
            μ.toMeasureOfZeroLE_apply_eq_enorm hs hpos hr,
            μ.toMeasureOfLEZero_apply_eq_enorm hs.compl hneg hr]
      _ ≤ μ.variation (s ∩ r) + μ.variation (sᶜ ∩ r) :=
          add_le_add (μ.enorm_measure_le_variation _) (μ.enorm_measure_le_variation _)
      _ = μ.variation ((s ∩ r) ∪ (sᶜ ∩ r)) :=
        (measure_union (by grind) (hs.compl.inter hr)).symm
      _ = μ.variation r := by congr; grind
  · apply VectorMeasure.variation_le_of_forall_enorm_le
    exact fun s _ ↦ enorm_le_totalVariation μ s

Goal state after: