internlm/Lean-Github huggingface dataset:
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:
specialize bh 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
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
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
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b
Tactic:
rw [ae_restrict_iff' sc.measurableSet]
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
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → ‖f n x‖ ≤ b
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
n : ℕ
bh : ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (x : X), x ∈ s → ‖f n x‖ ≤ b
Tactic:
exact ae_of_all _ bh
Proof state after:
no goals
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.h_lim
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
⊢ ∀ᵐ (a : X) ∂volume.restrict s, Tendsto (fun n => f n a) atTop (𝓝 (g a))
Tactic:
rw [ae_restrict_iff' sc.measurableSet]
Proof state after:
case intro.intro.h_lim
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
⊢ ∀ᵐ (x : X), x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.h_lim
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
⊢ ∀ᵐ (x : X), x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
Tactic:
apply ae_of_all
Proof state after:
case intro.intro.h_lim.a
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
⊢ ∀ a ∈ s, Tendsto (fun n => f n a) atTop (𝓝 (g a))
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.h_lim.a
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
⊢ ∀ a ∈ s, Tendsto (fun n => f n a) atTop (𝓝 (g a))
Tactic:
intro x xs
Proof state after:
case intro.intro.h_lim.a
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
x : X
xs : x ∈ s
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro.h_lim.a
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
x : X
xs : x ∈ s
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
Tactic:
exact u.tendsto_at xs
Proof state after:
no goals
Theorem: itau_volume
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
⊢ ↑volume itau = ENNReal.ofReal (2 * π)
Tactic:
simp only [itau, Real.volume_Ioc, sub_zero]
Proof state after:
no goals
Theorem: itau_real_volume
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
⊢ (↑volume itau).toReal = 2 * π
Tactic:
simp only [itau_volume, ENNReal.toReal_ofReal Real.two_pi_pos.le]
Proof state after:
no goals
Theorem: NiceVolume.itau
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
⊢ MeasurableSet _root_.itau
Tactic:
simp only [_root_.itau, gt_iff_lt, zero_lt_two, mul_pos_iff_of_pos_left, not_lt,
ge_iff_le, measurableSet_Ioc]
Proof state after:
no goals
Theorem: NiceVolume.itau
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
⊢ ↑volume _root_.itau < ⊤
Tactic:
simp only [itau_volume, ENNReal.ofReal_lt_top]
Proof state after:
no goals
Theorem: NiceVolume.itau
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
⊢ ↑volume _root_.itau > 0
Tactic:
simp only [itau_volume, gt_iff_lt, ENNReal.ofReal_pos, zero_lt_two,
mul_pos_iff_of_pos_left, Real.pi_pos]
Proof state after:
no goals
Theorem: measurableSet_itau
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
⊢ MeasurableSet itau
Tactic:
simp only [itau, measurableSet_Ioc]
Proof state after:
no goals
Theorem: tau_mem_itau
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
⊢ 2 * π ∈ itau
Tactic:
simp only [itau, Set.mem_Ioc, gt_iff_lt, zero_lt_two, mul_pos_iff_of_pos_left, Real.pi_pos,
  le_refl, and_self]
Proof state after:
no goals
Theorem: ContinuousOn.integrableOn_sphere
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
⊢ IntegrableOn (fun t => f (circleMap c r t)) itau volume
Tactic:
apply Continuous.integrableOn_Ioc
Proof state after:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
⊢ Continuous fun t => f (circleMap c r t)
Theorem: ContinuousOn.integrableOn_sphere
Proof state before:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
⊢ Continuous fun t => f (circleMap c r t)
Tactic:
apply fc.comp_continuous (continuous_circleMap _ _)
Proof state after:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
⊢ ∀ (x : ℝ), circleMap c r x ∈ closedBall c r
Theorem: ContinuousOn.integrableOn_sphere
Proof state before:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
⊢ ∀ (x : ℝ), circleMap c r x ∈ closedBall c r
Tactic:
intro t
Proof state after:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
t : ℝ
⊢ circleMap c r t ∈ closedBall c r
Theorem: ContinuousOn.integrableOn_sphere
Proof state before:
case hf
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 : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
rp : 0 < r
t : ℝ
⊢ circleMap c r t ∈ closedBall c r
Tactic:
simp only [Metric.mem_closedBall, Complex.dist_eq, circleMap_sub_center,
abs_circleMap_zero, abs_of_pos rp, le_refl]
Proof state after:
no goals
Theorem: Average.add
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 g : X → E
s : Set X
fi : IntegrableOn f s volume
gi : IntegrableOn g s volume
⊢ ⨍ (z : X) in s, f z + g z = (⨍ (z : X) in s, f z) + ⨍ (z : X) in s, g z
Tactic:
simp_rw [average_eq, integral_add fi gi, smul_add]
Proof state after:
no goals
Theorem: Average.sub
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 g : X → E
s : Set X
fi : IntegrableOn f s volume
gi : IntegrableOn g s volume
⊢ ⨍ (z : X) in s, f z - g z = (⨍ (z : X) in s, f z) - ⨍ (z : X) in s, g z
Tactic:
simp_rw [average_eq, integral_sub fi gi, smul_sub]
Proof state after:
no goals
Theorem: average_linear_comm
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ ⨍ (x : X) in s, g (f x) = g (⨍ (x : X) in s, f x)
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  LinearMapClass.map_smul]
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
f : X → E
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Theorem: average_linear_comm
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
by_cases v0 : (volume s).toReal = 0
Proof state after:
case pos
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : (↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

case neg
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Theorem: average_linear_comm
Proof state before:
case pos
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : (↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)

case neg
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)
Tactic:
simp [v0]
Proof state after:
case neg
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
s : Set X
fi : IntegrableOn f s volume
g : E →L[ℝ] F
v0 : ¬(↑volume s).toReal = 0
⊢ (↑volume s).toReal⁻¹ • ∫ (x : X) in s, g (f x) = (↑volume s).toReal⁻¹ • g (∫ (x : X) in s, f x)