internlm/Lean-Github huggingface dataset:
Theorem: RectangleBorderIntegrable.add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Tactic:
have h₃ := intervalIntegral.integral_add hf.2.2.1 hg.2.2.1
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
h₃ :
  ∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I) + g (↑w.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑w.re + ↑x * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Theorem: RectangleBorderIntegrable.add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g✝ : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f g : ℂ → E
hf : RectangleBorderIntegrable f z w
hg : RectangleBorderIntegrable g z w
h₁ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)
h₂ :
  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I) =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)
h₃ :
  ∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I) + g (↑w.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑w.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑w.re + ↑x * I)
h₄ :
  ∫ (x : ℝ) in z.im..w.im, f (↑z.re + ↑x * I) + g (↑z.re + ↑x * I) =
    (∫ (x : ℝ) in z.im..w.im, f (↑z.re + ↑x * I)) + ∫ (x : ℝ) in z.im..w.im, g (↑z.re + ↑x * I)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I) + g (↑x + ↑z.im * I)) -
          ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I) + g (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) + g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) + g (↑z.re + ↑y * I) =
    ((((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) +
      ((((∫ (x : ℝ) in z.re..w.re, g (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, g (↑x + ↑w.im * I)) +
          I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
        I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I))
Tactic:
additive_combination h₁ - h₂ + I • h₃ - I • h₄
Proof state after:
no goals
Theorem: ContinuousOn.rectangleBorder_integrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun x => ↑x + ↑z.im * I) [[z.re, w.re]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ContinuousOn.rectangleBorder_integrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun x => ↑x + ↑w.im * I) [[z.re, w.re]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ContinuousOn.rectangleBorder_integrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun y => ↑w.re + ↑y * I) [[z.im, w.im]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ContinuousOn.rectangleBorder_integrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (RectangleBorder z w)
⊢ ContinuousOn (fun y => ↑z.re + ↑y * I) [[z.im, w.im]]
Tactic:
fun_prop
Proof state after:
no goals
Theorem: ContinuousOn.rectangleBorderNoPIntegrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle z w \ {p})
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorderIntegrable f z w
Tactic:
refine (hf.mono (Set.subset_diff.mpr ?_)).rectangleBorder_integrable
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle z w \ {p})
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Theorem: ContinuousOn.rectangleBorderNoPIntegrable
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hf : ContinuousOn f (Rectangle z w \ {p})
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
Tactic:
exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
Proof state after:
no goals
Theorem: RectangleIntegralHSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ RectangleIntegral f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I) =
    RectangleIntegral f (↑x₀ + ↑y₀ * I) (↑a + ↑y₁ * I) + RectangleIntegral f (↑a + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
Tactic:
dsimp [RectangleIntegral, HIntegral, VIntegral]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..a + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..a + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(a + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in a + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in a + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(a + (y₀ * 0 - 0 * 1)) + ↑y * I))
Theorem: RectangleIntegralHSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..a + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..a + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(a + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in a + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in a + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(a + (y₀ * 0 - 0 * 1)) + ↑y * I))
Tactic:
ring_nf
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Theorem: RectangleIntegralHSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Tactic:
have h₁ := intervalIntegral.integral_add_adjacent_intervals f_int_x₀_a_bot f_int_a_x₁_bot
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
h₁ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Theorem: RectangleIntegralHSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
h₁ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Tactic:
have h₂ := intervalIntegral.integral_add_adjacent_intervals f_int_x₀_a_top f_int_a_x₁_top
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
h₁ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)
h₂ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Theorem: RectangleIntegralHSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
f_int_x₀_a_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ a
f_int_a_x₁_bot : IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume a x₁
f_int_x₀_a_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ a
f_int_a_x₁_top : IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume a x₁
h₁ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)
h₂ :
  (∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) + ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I) = ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)
⊢ (((∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..x₁, f (↑x + ↑y₁ * I)) +
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
      I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I) =
    ((((∫ (x : ℝ) in x₀..a, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in x₀..a, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑x₀ + ↑y * I)) +
      ((((∫ (x : ℝ) in a..x₁, f (↑x + ↑y₀ * I)) - ∫ (x : ℝ) in a..x₁, f (↑x + ↑y₁ * I)) +
          I • ∫ (y : ℝ) in y₀..y₁, f (↑x₁ + ↑y * I)) -
        I • ∫ (y : ℝ) in y₀..y₁, f (↑a + ↑y * I))
Tactic:
additive_combination - h₁ + h₂
Proof state after:
no goals
Theorem: RectangleIntegralHSplit'
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
ha : a ∈ [[x₀, x₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun x => f (↑x + ↑y₀ * I)) volume x₀ x₁
Tactic:
simpa using hf.1
Proof state after:
no goals
Theorem: RectangleIntegralHSplit'
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ a x₀ x₁ y₀ y₁ : ℝ
ha : a ∈ [[x₀, x₁]]
hf : RectangleBorderIntegrable f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I)
⊢ IntervalIntegrable (fun x => f (↑x + ↑y₁ * I)) volume x₀ x₁
Tactic:
simpa using hf.2.1
Proof state after:
no goals
Theorem: RectangleIntegralVSplit
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
⊢ RectangleIntegral f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑y₁ * I) =
    RectangleIntegral f (↑x₀ + ↑y₀ * I) (↑x₁ + ↑b * I) + RectangleIntegral f (↑x₀ + ↑b * I) (↑x₁ + ↑y₁ * I)
Tactic:
dsimp [RectangleIntegral, HIntegral, VIntegral]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁✝ x₂ y y₁✝ y₂ σ b x₀ x₁ y₀ y₁ : ℝ
f_int_y₀_b_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume y₀ b
f_int_b_y₁_left : IntervalIntegrable (fun y => f (↑x₀ + ↑y * I)) volume b y₁
f_int_y₀_b_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume y₀ b
f_int_b_y₁_right : IntervalIntegrable (fun y => f (↑x₁ + ↑y * I)) volume b y₁
⊢ (((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
          ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
      I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I) =
    ((((∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (y₀ * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (y₀ * 0 - 0 * 1)..x₁ + (b * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₁ + (b * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (y₀ * 1 + 0 * 0)..0 + (b * 1 + 0 * 0), f (↑(x₀ + (y₀ * 0 - 0 * 1)) + ↑y * I)) +
      ((((∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (b * 1 + 0 * 0)) * I)) -
            ∫ (x : ℝ) in x₀ + (b * 0 - 0 * 1)..x₁ + (y₁ * 0 - 0 * 1), f (↑x + ↑(0 + (y₁ * 1 + 0 * 0)) * I)) +
          I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₁ + (y₁ * 0 - 0 * 1)) + ↑y * I)) -
        I • ∫ (y : ℝ) in 0 + (b * 1 + 0 * 0)..0 + (y₁ * 1 + 0 * 0), f (↑(x₀ + (b * 0 - 0 * 1)) + ↑y * I))