internlm/Lean-Github huggingface dataset:
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
rw [integer_linear, ContinuousMap.coe_mk]
Proof state after:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (↑n * ↑y)).exp‖₊
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (↑n * ↑y)).exp‖₊
Tactic:
congr
Proof state after:
case h.h.h.h.a.e_a.e_a.e_f
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun y => K x y * f y * (Complex.I * (↑n * ↑y)).exp
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h.a.e_a.e_a.e_f
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun y => K x y * f y * (Complex.I * (↑n * ↑y)).exp
Tactic:
ext y
Proof state after:
case h.h.h.h.a.e_a.e_a.e_f.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = K x y * f y * (Complex.I * (↑n * ↑y)).exp
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
case h.h.h.h.a.e_a.e_a.e_f.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = K x y * f y * (Complex.I * (↑n * ↑y)).exp
Tactic:
ring_nf
Proof state after:
no goals
Theorem: CarlesonOperatorReal'_le_CarlesonOperator'
Proof state before:
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ θ n ∈ {x | ∃ n, θ n = x}
Tactic:
simp
Proof state after:
no goals
Theorem: rcarleson'
Proof state before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, T' f x ≤ ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
calc ∫⁻ x in G, T' f x
  _ ≤ ∫⁻ x in G, CarlesonOperator' K Θ f x := by
    apply MeasureTheory.lintegral_mono
    apply CarlesonOperatorReal'_le_CarlesonOperator'
  _ ≤ ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by
    convert theorem1_2C' K (by simp) h1 h2 hF hG h3 f hf <;> sorry
Proof state after:
no goals
Theorem: rcarleson'
Proof state before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, T' f x ≤ ∫⁻ (x : ℝ) in G, CarlesonOperator' K {x | ∃ n, θ n = x} f x
Tactic:
apply MeasureTheory.lintegral_mono
Proof state after:
case hfg
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ (fun a => T' f a) ≤ fun a => CarlesonOperator' K {x | ∃ n, θ n = x} f a
Theorem: rcarleson'
Proof state before:
case hfg
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ (fun a => T' f a) ≤ fun a => CarlesonOperator' K {x | ∃ n, θ n = x} f a
Tactic:
apply CarlesonOperatorReal'_le_CarlesonOperator'
Proof state after:
no goals
Theorem: rcarleson'
Proof state before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, CarlesonOperator' K {x | ∃ n, θ n = x} f x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
convert theorem1_2C' K (by simp) h1 h2 hF hG h3 f hf <;> sorry
Proof state after:
no goals
Theorem: rcarleson'
Proof state before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ 4 ≤ 4
Tactic:
simp
Proof state after:
no goals
Theorem: prop2_3
Proof state before:
X : Type u_1
A : ℝ
inst✝⁶ : MetricSpace X
inst✝⁵ : IsSpaceOfHomogeneousType X A
inst✝⁴ : Inhabited X
τ q D κ ε δ C₀ C t : ℝ
Θ : Set C(X, ℂ)
inst✝³ : IsCompatible Θ
inst✝² : IsCancellative τ Θ
inst✝¹ : TileStructure Θ D κ C₀
F G : Set X
σ σ' : X → ℤ
Q' : X → C(X, ℂ)
K : X → X → ℂ
inst✝ : IsCZKernel τ K
ψ : ℝ → ℝ
n : ℕ
𝔉 : Forest G Q' δ n
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hC₀ : 0 < C₀
hC : C2_3 A τ q C₀ < C
hκ : κ ∈ Ioo 0 (κ2_3 A τ q C₀)
hε : ε ∈ Ioo 0 (ε2_3 A τ q C₀)
hδ : δ ∈ Ioo 0 (δ2_3 A τ q C₀)
hD : (2 * A) ^ 100 < D
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
Q'_mem : ∀ (x : X), Q' x ∈ Θ
m_Q' : Measurable Q'
m_σ : Measurable σ
m_σ' : Measurable σ'
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
hψ : LipschitzWith (Cψ2_3 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
ht : t ∈ Ioc 0 1
h𝔉 : 𝔉.carrier ⊆ boundedTiles F t
⊢ ↑‖∑ᶠ (p : 𝔓 X) (_ : p ∈ 𝔉.carrier), TL K Q' σ σ' ψ p F‖₊ ≤ C * 2 ^ (-ε * ↑n) * t ^ (1 / q - 1 / 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: Memℒp_T
Proof state before:
X : Type u_1
A : ℝ
inst✝³ : PseudoMetricSpace X
inst✝² : IsSpaceOfHomogeneousType X A
D κ C : ℝ
inst✝¹ : Inhabited X
Θ : Set C(X, ℂ)
inst✝ : TileStructure Θ D κ C
K : X → X → ℂ
Q' : X → C(X, ℂ)
σ σ' : X → ℤ
ψ : ℝ → ℝ
p : 𝔓 X
F : Set X
f : X → ℂ
q : ℝ≥0∞
hf : Memℒp f q volume
⊢ Memℒp (T K Q' σ σ' ψ p F f) q volume
Tactic:
sorry
Proof state after:
no goals
Theorem: Finset.sum_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x ∈ s, μ {x} = μ ↑s
Tactic:
change ∑ x in s, μ (id ⁻¹' {x}) = _
Proof state after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s
Theorem: Finset.sum_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s
Tactic:
rw [sum_measure_preimage_singleton]
Proof state after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ μ (id ⁻¹' ↑s) = μ ↑s

case hf
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})
Theorem: Finset.sum_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ μ (id ⁻¹' ↑s) = μ ↑s
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.sum_measure_singleton
Proof state before:
case hf
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.sum_toReal_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ ∑ x ∈ s, (μ {x}).toReal = (μ ↑s).toReal
Tactic:
rw [← ENNReal.toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
Proof state after:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ (∑ a ∈ s, μ {a}).toReal = (μ ↑s).toReal
Theorem: Finset.sum_toReal_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
s : Finset S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ (∑ a ∈ s, μ {a}).toReal = (μ ↑s).toReal
Tactic:
simp
Proof state after:
no goals
Theorem: sum_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
inst✝¹ : Fintype S
x✝ : MeasurableSpace S
inst✝ : MeasurableSingletonClass S
μ : Measure S
⊢ ∑ x : S, μ {x} = μ univ
Tactic:
simp
Proof state after:
no goals
Theorem: sum_toReal_measure_singleton
Proof state before:
ι : Type u_1
S : Type u_2
inst✝² : Fintype S
x✝ : MeasurableSpace S
inst✝¹ : MeasurableSingletonClass S
μ : Measure S
inst✝ : IsFiniteMeasure μ
⊢ ∑ x : S, (μ {x}).toReal = (μ univ).toReal
Tactic:
simp
Proof state after:
no goals
Theorem: MeasureTheory.measure_diff_eq_top
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : μ s = ⊤
ht : μ t ≠ ⊤
⊢ μ (s \ t) = ⊤
Tactic:
contrapose! hs
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ s ≠ ⊤
Theorem: MeasureTheory.measure_diff_eq_top
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ s ≠ ⊤
Tactic:
apply ((measure_mono (subset_diff_union s t)).trans_lt _).ne
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t ∪ t) < ⊤
Theorem: MeasureTheory.measure_diff_eq_top
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t ∪ t) < ⊤
Tactic:
apply (measure_union_le _ _).trans_lt
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t) + μ t < ⊤
Theorem: MeasureTheory.measure_diff_eq_top
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t) + μ t < ⊤
Tactic:
exact ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_eq_zero_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real s = 0 ↔ μ s = 0
Tactic:
rw [Measure.real, ENNReal.toReal_eq_zero_iff]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ s = 0 ∨ μ s = ⊤ ↔ μ s = 0
Theorem: MeasureTheory.measureReal_eq_zero_iff
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ s = 0 ∨ μ s = ⊤ ↔ μ s = 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ Measure.real 0 s = 0
Tactic:
simp [measureReal_def]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_empty
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
⊢ μ.real ∅ = 0
Tactic:
simp [Measure.real]
Proof state after:
no goals
Theorem: MeasureTheory.IsProbabilityMeasure.measureReal_univ
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : IsProbabilityMeasure μ
⊢ μ.real univ = 1
Tactic:
simp [Measure.real]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_univ_pos
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < μ.real univ
Tactic:
rw [measureReal_def]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < (μ univ).toReal
Theorem: MeasureTheory.measureReal_univ_pos
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ 0 < (μ univ).toReal
Tactic:
apply ENNReal.toReal_pos
Proof state after:
case ha₀
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ 0

case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Theorem: MeasureTheory.measureReal_univ_pos
Proof state before:
case ha₀
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ 0

case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Tactic:
exact NeZero.ne (μ Set.univ)
Proof state after:
case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Theorem: MeasureTheory.measureReal_univ_pos
Proof state before:
case ha_top
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ⊤
Tactic:
finiteness
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_smul_apply
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ (c • μ).real s = c.toReal • μ.real s
Tactic:
rw [measureReal_def, smul_apply, smul_eq_mul, ENNReal.toReal_mul]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ c.toReal * (μ s).toReal = c.toReal • μ.real s
Theorem: MeasureTheory.measureReal_smul_apply
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
c : ℝ≥0∞
⊢ c.toReal * (μ s).toReal = c.toReal • μ.real s
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.map_measureReal_apply
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f μ).real s = μ.real (f ⁻¹' s)
Tactic:
rw [measureReal_def, map_apply hf hs]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (μ (f ⁻¹' s)).toReal = μ.real (f ⁻¹' s)
Theorem: MeasureTheory.map_measureReal_apply
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (μ (f ⁻¹' s)).toReal = μ.real (f ⁻¹' s)
Tactic:
rfl
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_mono_null
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0
Tactic:
rw [measureReal_eq_zero_iff h'₂] at h₂
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₁ ⊆ s₂
h₂ : μ s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0
Theorem: MeasureTheory.measureReal_mono_null
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₁ ⊆ s₂
h₂ : μ s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0
Tactic:
simp [Measure.real, measure_mono_null h h₂]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_le_measureReal_union_left
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
rcases eq_top_or_lt_top (μ s) with hs|hs
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s = ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s < ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)
Theorem: MeasureTheory.measureReal_le_measureReal_union_left
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s = ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
simp [Measure.real, hs]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_le_measureReal_union_left
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ t ≠ ⊤) _auto✝
hs : μ s < ⊤
⊢ μ.real s ≤ μ.real (s ∪ t)
Tactic:
exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_le_measureReal_union_right
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real t ≤ μ.real (s ∪ t)
Tactic:
rw [union_comm]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real t ≤ μ.real (t ∪ s)
Theorem: MeasureTheory.measureReal_le_measureReal_union_right
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : autoParam (μ s ≠ ⊤) _auto✝
⊢ μ.real t ≤ μ.real (t ∪ s)
Tactic:
exact measureReal_le_measureReal_union_left h
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h|h
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
simp only [Measure.real, h, ENNReal.top_toReal]
Proof state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ 0 ≤ (μ s₁).toReal + (μ s₂).toReal
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) = ⊤
⊢ 0 ≤ (μ s₁).toReal + (μ s₂).toReal
Tactic:
exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
Proof state after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
Proof state after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic:
simp only [Measure.real, ← ENNReal.toReal_add A B]
Proof state after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ (μ (s₁ ∪ s₂)).toReal ≤ (μ s₁ + μ s₂).toReal
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ (μ (s₁ ∪ s₂)).toReal ≤ (μ s₁ + μ s₂).toReal
Tactic:
exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_union_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ⊤
A : μ s₁ ≠ ⊤
B : μ s₂ ≠ ⊤
⊢ μ s₁ + μ s₂ ≠ ⊤
Tactic:
simp [A, B]
Proof state after:
no goals
Theorem: MeasureTheory.measureReal_biUnion_finset_le
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
Tactic:
induction' s using Finset.induction_on with x s hx IH
Proof state after:
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
f : β → Set α
⊢ μ.real (⋃ b ∈ ∅, f b) ≤ ∑ p ∈ ∅, μ.real (f p)

case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (⋃ b ∈ insert x s, f b) ≤ ∑ p ∈ insert x s, μ.real (f p)
Theorem: MeasureTheory.measureReal_biUnion_finset_le
Proof state before:
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
f : β → Set α
⊢ μ.real (⋃ b ∈ ∅, f b) ≤ ∑ p ∈ ∅, μ.real (f p)
Tactic:
simp
Proof state after:
no goals