internlm/Lean-Github huggingface dataset:
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rcases le_total a b with hab | hab
Proof state after:
case inl
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case inr
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case inl
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [intervalIntegral.integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
← integral_indicator measurableSet_Icc, indicator_eq_self.2 h]
Proof state after:
no goals
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case inr
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
by_cases hab2 : b = a
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [hab2] at h ⊢
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..a, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ ∫ (x : ℝ) in a..a, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
simp only [intervalIntegral.integral_same]
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a a
hab : b ≤ a
hab2 : b = a
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
simp only [Icc_self] at h
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by
  rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [this, integral_singleton]
Proof state after:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = (μ {a}).toReal • f a
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = (μ {a}).toReal • f a
Tactic:
simp
Proof state after:
no goals
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
Tactic:
rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
Proof state after:
no goals
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ MeasurableSet {a}
Tactic:
simp
Proof state after:
no goals
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
rw [Icc_eq_empty_iff.mpr <| by exact fun x ↦ hab2 <| le_antisymm hab x, subset_empty_iff,
    Function.support_eq_empty_iff] at h
Proof state after:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : f = 0
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
case neg
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : f = 0
hab : b ≤ a
hab2 : ¬b = a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: IntervalIntegral.integral_eq_integral_of_support_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
h : Function.support f ⊆ Icc a b
hab : b ≤ a
hab2 : ¬b = a
⊢ ¬a ≤ b
Tactic:
exact fun x ↦ hab2 <| le_antisymm hab x
Proof state after:
no goals
Theorem: SetIntegral.integral_eq_integral_inter_of_support_subset
Proof state before:
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
μ : Measure ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set ℝ
f : ℝ → E
h : Function.support f ⊆ t
ht : MeasurableSet t
⊢ ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in s ∩ t, f x ∂μ
Tactic:
rw [← setIntegral_indicator ht, indicator_eq_self.2 h]
Proof state after:
no goals
Theorem: SetIntegral.integral_eq_integral_inter_of_support_subset_Icc
Proof state before:
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
f : ℝ → E
h : Function.support f ⊆ Icc a b
hs : Icc a b ⊆ s
⊢ ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in Icc a b, f x ∂μ
Tactic:
rw [SetIntegral.integral_eq_integral_inter_of_support_subset h measurableSet_Icc,
    inter_eq_self_of_subset_right hs]
Proof state after:
no goals
Theorem: intervalIntegral.norm_integral_le_of_norm_le_const'
Proof state before:
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b C : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hab : a ≤ b
h : ∀ x ∈ Icc a b, ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le_const
Proof state after:
case h
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b C : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hab : a ≤ b
h : ∀ x ∈ Icc a b, ‖f x‖ ≤ C
⊢ ∀ x ∈ Ι a b, ‖f x‖ ≤ C
Theorem: intervalIntegral.norm_integral_le_of_norm_le_const'
Proof state before:
case h
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b C : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hab : a ≤ b
h : ∀ x ∈ Icc a b, ‖f x‖ ≤ C
⊢ ∀ x ∈ Ι a b, ‖f x‖ ≤ C
Tactic:
exact fun x hx ↦ h x <| mem_Icc_of_Ioc <| uIoc_of_le hab ▸ hx
Proof state after:
no goals
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ Tendsto f (𝓝[>] 0) (𝓝 0)
Tactic:
apply Tendsto.comp (tendsto_nhds_of_eventually_eq ?_) tendsto_id
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x' : ℝ) in 𝓝[>] 0, f x' = 0
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x' : ℝ) in 𝓝[>] 0, f x' = 0
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' ha] with c hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ f c = 0
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ f c = 0
Tactic:
replace hc := (mem_Ioo.mp hc).2
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
⊢ f c = 0
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
⊢ f c = 0
Tactic:
have h : c ∉ Icc a b := fun h ↦ by linarith [mem_Icc.mp h]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0
Tactic:
convert mt (Function.support_subset_iff.mp fSupp c) h
Proof state after:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Filter.TendstoAtZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h]
Proof state after:
no goals
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ Tendsto f atTop (𝓝 0)
Tactic:
apply Tendsto.comp (tendsto_nhds_of_eventually_eq ?_) tendsto_id
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x' : ℝ) in atTop, f x' = 0
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x' : ℝ) in atTop, f x' = 0
Tactic:
filter_upwards [Ioi_mem_atTop b] with c hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioi b
⊢ f c = 0
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioi b
⊢ f c = 0
Tactic:
rw [mem_Ioi] at hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ f c = 0
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ f c = 0
Tactic:
have h : c ∉ Icc a b := fun h ↦ by linarith [mem_Icc.mp h]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∉ Icc a b
⊢ f c = 0
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∉ Icc a b
⊢ f c = 0
Tactic:
convert mt (Function.support_subset_iff.mp fSupp c) h
Proof state after:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Filter.TendstoAtTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h]
Proof state after:
no goals
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ f =O[𝓝[>] 0] fun x => 0
Tactic:
refine Eventually.isBigO ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖f x‖ ≤ 0
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖f x‖ ≤ 0
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < a)] with c hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ ‖f c‖ ≤ 0
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ ‖f c‖ ≤ 0
Tactic:
refine norm_le_zero_iff.mpr <| Function.support_subset_iff'.mp fSupp c ?_
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ c ∉ Icc a b
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ c ∉ Icc a b
Tactic:
exact fun h ↦ by linarith [mem_Icc.mp h, (mem_Ioo.mp hc).2]
Proof state after:
no goals
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ 0 < a
Tactic:
linarith
Proof state after:
no goals
Theorem: Filter.BigO_zero_atZero_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h, (mem_Ioo.mp hc).2]
Proof state after:
no goals
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ f =O[atTop] fun x => 0
Tactic:
refine Eventually.isBigO ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ 0
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ 0
Tactic:
filter_upwards [Ioi_mem_atTop b] with c hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioi b
⊢ ‖f c‖ ≤ 0
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioi b
⊢ ‖f c‖ ≤ 0
Tactic:
replace hc := mem_Ioi.mp hc
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ ‖f c‖ ≤ 0
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ ‖f c‖ ≤ 0
Tactic:
refine norm_le_zero_iff.mpr <| Function.support_subset_iff'.mp fSupp c ?_
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ c ∉ Icc a b
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
⊢ c ∉ Icc a b
Tactic:
exact fun h ↦ by linarith [mem_Icc.mp h]
Proof state after:
no goals
Theorem: Filter.BigO_zero_atTop_of_support_in_Icc
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : b < c
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h]
Proof state after:
no goals
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ ∃ u', u = ↑u' ∧ HasDerivAt f u' z
Tactic:
lift u to ℝ
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0

case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z
Tactic:
refine ⟨u, rfl, ?_⟩
Proof state after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z
Tactic:
convert (reCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt
Proof state after:
case h.e'_7
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case h.e'_7
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
Tactic:
rw [comp_apply, smulRight_apply, one_apply, one_smul, reCLM_apply, ofReal_re]
Proof state after:
no goals
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0
Tactic:
have H := (imCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt.deriv
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
simp only [Function.comp_def, imCLM_apply, ofReal_im, deriv_const] at H
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
rwa [eq_comm, comp_apply, imCLM_apply, smulRight_apply, one_apply, one_smul] at H
Proof state after:
no goals
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) z ↔ DifferentiableAt ℝ f z
Tactic:
refine ⟨fun H ↦ ?_, ofReal_comp⟩
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z
Tactic:
obtain ⟨u, _, hu₂⟩ := H.hasDerivAt.of_hasDerivAt_ofReal_comp
Proof state after:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z