internlm/Lean-Github huggingface dataset:
Theorem: osgood
Proof state before:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
have rs : closedBall c (r / 2) ⊆ s := le_trans (Metric.closedBall_subset_ball (by linarith)) rs
Proof state after:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
case intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases ((isCompact_closedBall _ _).bddAbove_image (ContinuousOn.mono fc rs).norm).exists_ge 0
  with ⟨b, bp, bh⟩
Proof state after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ y ∈ (fun x => ‖f x‖) '' closedBall c (r / 2), y ≤ b
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ y ∈ (fun x => ‖f x‖) '' closedBall c (r / 2), y ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
simp only [Set.forall_mem_image] at bh
Proof state after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
have h : Separate f c.fst c.snd (r / 2) b s :=
  { rp := by linarith
    so := o
    rs := rs
    fc := fc
    fa0 := fa0 _ _
    fa1 := fa1 _ _
    bp := bp
    fb := fun {z0 z1} z0m z1m ↦ @bh (z0, z1)
      (spheres_subset_closedBall (Set.mk_mem_prod z0m z1m)) }
Proof state after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
⊢ AnalyticAt ℂ f c
Tactic:
have a := (osgood_h h).analyticAt
Proof state after:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
a : AnalyticAt ℂ f (c.1, c.2)
⊢ AnalyticAt ℂ f c
Theorem: osgood
Proof state before:
case intro.intro.intro.intro
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
h : Separate f c.1 c.2 (r / 2) b s
a : AnalyticAt ℂ f (c.1, c.2)
⊢ AnalyticAt ℂ f c
Tactic:
simpa only [Prod.mk.eta] using a
Proof state after:
no goals
Theorem: osgood
Proof state before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ r / 2 < r
Tactic:
linarith
Proof state after:
no goals
Theorem: osgood
Proof state before:
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
fc : ContinuousOn f s
fa0 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
fa1 : ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs✝ : ball c r ⊆ s
rs : closedBall c (r / 2) ⊆ s
b : ℝ
bp : 0 ≤ b
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ closedBall c (r / 2) → ‖f x‖ ≤ b
⊢ 0 < r / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: osgood_at'
Proof state before:
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
⊢ AnalyticAt ℂ f c
Tactic:
rcases eventually_nhds_iff.mp h with ⟨s, h, o, cs⟩
Proof state after:
case intro.intro.intro
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h✝ :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
s : Set (ℂ × ℂ)
h : ∀ x ∈ s, ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Theorem: osgood_at'
Proof state before:
case intro.intro.intro
E : Type
f : ℂ × ℂ → E
c : ℂ × ℂ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
h✝ :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 c,
    ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
s : Set (ℂ × ℂ)
h : ∀ x ∈ s, ContinuousAt f x ∧ AnalyticAt ℂ (fun z => f (z, x.2)) x.1 ∧ AnalyticAt ℂ (fun z => f (x.1, z)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
exact osgood o (fun _ m ↦ (h _ m).1.continuousWithinAt) (fun _ _ m ↦ (h _ m).2.1)
  (fun _ _ m ↦ (h _ m).2.2) c cs
Proof state after:
no goals
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
⊢ volume.ae.EventuallyEq s (s \ t)
Tactic:
simp only [Filter.EventuallyEq, Pi.sdiff_apply, eq_iff_iff]
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Tactic:
have e : ∀ x, x ∉ t → (x ∈ s ↔ x ∈ s \ t) := by
  intro x h; simp only [Set.mem_diff, h, not_false_iff, and_true_iff]
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ x ∉ t, x ∈ s ↔ x ∈ s \ t
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ x ∉ t, x ∈ s ↔ x ∈ s \ t
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Tactic:
simp_rw [Set.mem_def] at e
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ∀ᵐ (x : X), s x ↔ s x \ t x
Tactic:
refine Filter.Eventually.mono ?_ e
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ∀ᵐ (x : X), ¬t x
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ∀ᵐ (x : X), ¬t x
Tactic:
rw [ae_iff]
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ↑volume {a | ¬¬t a} = 0
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
e : ∀ (x : X), ¬t x → (s x ↔ (s \ t) x)
⊢ ↑volume {a | ¬¬t a} = 0
Tactic:
simpa [Set.setOf_set]
Proof state after:
no goals
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
⊢ ∀ x ∉ t, x ∈ s ↔ x ∈ s \ t
Tactic:
intro x h
Proof state after:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
x : X
h : x ∉ t
⊢ x ∈ s ↔ x ∈ s \ t
Theorem: ae_minus_null
Proof state before:
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
s t : Set X
tz : ↑volume t = 0
x : X
h : x ∉ t
⊢ x ∈ s ↔ x ∈ s \ t
Tactic:
simp only [Set.mem_diff, h, not_false_iff, and_true_iff]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))
Tactic:
rcases u.uniformCauchySeqOn.bounded fc sc with ⟨b, _, bh⟩
Proof state after:
case intro.intro
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), AEStronglyMeasurable (f n) (volume.restrict s)
Tactic:
intro n
Proof state after:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ AEStronglyMeasurable (f n) (volume.restrict s)
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ AEStronglyMeasurable (f n) (volume.restrict s)
Tactic:
exact (fc n).aestronglyMeasurable sc.measurableSet
Proof state after:
no goals
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.bound_integrable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Integrable (fun x => b) (volume.restrict s)
Tactic:
exact continuousOn_const.integrableOn_compact sc
Proof state after:
no goals
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
Tactic:
intro n
Proof state after:
case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
n : ℕ
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b