mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ ∫⁻ (a : α), ↑f a ∂μ = f.lintegral

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₘ[μ] ℝ≥0∞
f : α → ℝ≥0∞
hf : AEStronglyMeasurable f μ
g : α → ℝ≥0∞
x✝ : AEStronglyMeasurable g μ
⊢ (mk f hf + mk g x✝).lintegral = (mk f hf).lintegral + (mk g x✝).lintegral

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x ↦ rexp (f x)) μ
⊢ AEMeasurable f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (fun x ↦ rexp (t * f x)) μ
⊢ AEMeasurable f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurableSet {a | 0 ≤ a.re}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin (x.im / ‖x‖)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurableSet {a | 0 ≤ a.im}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin ((-x).im / ‖x‖) + Real.pi

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun x ↦ Real.arcsin ((-x).im / ‖x‖) - Real.pi

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable fun x ↦ ↑(f x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ ↑(f x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurableSet {a | a.1 = 0}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurableSet {a | a.2 = 0}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun p ↦ cexp (log p.1 * p.2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑p.1 ^ ↑p.2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑p.1 ^ p.2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurableSet {a | a.1 = 0 ∧ a.2 < 0}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ Measurable fun p ↦ ↑(p.1 ^ p.2)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: ⊢ MeasurablePow ℝ≥0∞ ℝ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑|f| =ᵐ[μ] fun x ↦ |↑f x|

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : TopologicalSpace δ
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
R : Type u_5
inst✝² : TopologicalSpace R
inst✝¹ : InvolutiveStar R
inst✝ : ContinuousStar R
f : α →ₘ[μ] R
⊢ comp (star ∘ star) ⋯ f = f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : TopologicalSpace δ
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LinearOrder γ
inst✝¹ : OrderClosedTopology γ
inst✝ : Zero γ
f : α →ₘ[μ] γ
⊢ Continuous[inst✝³, inst✝³] fun x ↦ max x 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : TopologicalSpace δ
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LinearOrder γ
inst✝¹ : OrderClosedTopology γ
inst✝ : Zero γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ max (f x) 0) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
ι : Type u_5
inst✝¹ : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst✝ : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f i ω) l (𝓝 (h ω))
⊢ g =ᵐ[μ] h

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurableSpace.pi ≤ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure).caratheodory

Tactic:
refine iSup_le ?_
  intro i s hs
  rw [MeasurableSpace.comap] at hs
  rcases hs with ⟨s, hs, rfl⟩
  apply boundedBy_caratheodory
  intro t
  simp_rw [piPremeasure]
  refine Finset.prod_add_prod_le' (Finset.mem_univ i) ?_ ?_ ?_
  · simp [image_inter_preimage, image_sdiff_preimage, measure_inter_add_sdiff _ hs]
  · rintro j - _; gcongr; apply inter_subset_left
  · rintro j - _; gcongr; apply sdiff_subset

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurableSpace.pi ≤ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure).caratheodory

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this✝ : Encodable ι
this : (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure
⊢ (pi' μ) (univ.pi s) ≤ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure) (univ.pi s)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ ∏ i, (μ i) (toMeasurable (μ i) ((hμ i).set (e n i))) = ∏ i, (μ i) ((hμ i).set (e n i))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
⊢ (Measure.pi μ).FiniteSpanningSetsIn (univ.pi '' univ.pi C)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
i : ι
⊢ MeasurableSpace (α i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
⊢ ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
⊢ Measure.pi μ = μν

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ (Measure.pi μ) univ = ∏ i, (μ i) univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
f : (i : ι) → α i
⊢ (Measure.pi μ) {f} = ∏ i, (μ i) {f i}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ (Measure.pi μ) univ = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ (Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ (Measure.pi μ) (Metric.ball x r) = ∏ i, (μ i) (Metric.ball (x i) r)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (Metric.closedBall x r) = ∏ i, (μ i) (Metric.closedBall (x i) r)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
⊢ Measure.pi μ = dirac x

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (α : α) → MeasurableSpace (β α)
μ : (a : α) → Measure (β a)
⊢ (Measure.pi μ) univ = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : (μ i) s = 0
⊢ (Measure.pi μ) (eval i ⁻¹' s) = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ Measurable (eval i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : MeasurableSet s
h2s : (μ i) s = 0
⊢ Measurable (eval i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
⊢ QuasiMeasurePreserving (eval i) (Measure.pi μ) (μ i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ i ∈ Finset.univ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
⊢ map (eval i) (Measure.pi μ) = (∏ j ∈ Finset.univ.erase i, (μ j) univ) • μ i

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / p.toReal * p.toReal = 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε ^ p.toReal * μ {x | ε ≤ ‖f x‖ₑ} ≤ eLpNorm f p μ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ε = ∞
⊢ 0 ^ p.toReal = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
⊢ ε ^ p.toReal ≠ ∞

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
⊢ μ {x | ε ≤ ‖f x‖ₑ} < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ∞
⊢ ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ↑ε ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ε ≤ ‖f x‖₊} < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Indicator

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Indicator

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖t.indicator f a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖f a‖

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
⊢ map (fun x i ↦ f i (x i)) (Measure.pi μ) = Measure.pi fun i ↦ map (f i) (μ i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ MeasurePreserving (eval i) (Measure.pi μ) (μ i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi μ).restrict (univ.pi fun i ↦ s i) = Measure.pi fun i ↦ (μ i).restrict (s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
⊢ eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
by

Goal state after: