internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.h
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
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ioc a b
y : X
ys : y ∈ s
⊢ (fun x => (x, t)) y ∈ s ×ˢ Icc a b
Tactic:
exact Set.mk_mem_prod ys (Set.Ioc_subset_Icc_self ts)
Proof state after:
no goals
Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro.h_cont.a.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
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
t : ℝ
ts : t ∈ Ι a b
⊢ x ∈ s
Tactic:
assumption
Proof state after:
no goals
Theorem: aEMeasurable_liminf'
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => liminf (fun n => f n x) u) μ
Tactic:
simp_rw [uc.toHasBasis.liminf_eq_iSup_iInf]
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, f a x) μ
Theorem: aEMeasurable_liminf'
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ AEMeasurable (fun x => ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, f a x) μ
Tactic:
refine aemeasurable_biSup _ uc.countable ?_
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ ∀ i ∈ fun i => p i, AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Theorem: aEMeasurable_liminf'
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
⊢ ∀ i ∈ fun i => p i, AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Tactic:
intro i _
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
i : I'
a✝ : i ∈ fun i => p i
⊢ AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Theorem: aEMeasurable_liminf'
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
I I' : Type
u : Filter I
f : I → X → ℝ≥0∞
μ : Measure X
p : I' → Prop
s : I' → Set I
fm : ∀ (n : I), AEMeasurable (f n) μ
uc : u.HasCountableBasis p s
sc : ∀ (i : I'), (s i).Countable
i : I'
a✝ : i ∈ fun i => p i
⊢ AEMeasurable (fun x => ⨅ a ∈ s i, f a x) μ
Tactic:
exact aemeasurable_biInf _ (sc i) (fun n _ ↦ fm n)
Proof state after:
no goals
Theorem: set_lintegral_mono_aEMeasurable
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 : Set X
f g : X → ℝ≥0∞
sm : MeasurableSet s
fg : ∀ x ∈ s, f x ≤ g x
⊢ ∫⁻ (x : X) in s, f x ≤ ∫⁻ (x : X) in s, g x
Tactic:
apply lintegral_mono_ae
Proof state after:
case h
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 : Set X
f g : X → ℝ≥0∞
sm : MeasurableSet s
fg : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (a : X) ∂volume.restrict s, f a ≤ g a
Theorem: set_lintegral_mono_aEMeasurable
Proof state before:
case h
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 : Set X
f g : X → ℝ≥0∞
sm : MeasurableSet s
fg : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (a : X) ∂volume.restrict s, f a ≤ g a
Tactic:
rw [ae_restrict_iff' sm]
Proof state after:
case h
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 : Set X
f g : X → ℝ≥0∞
sm : MeasurableSet s
fg : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : X), x ∈ s → f x ≤ g x
Theorem: set_lintegral_mono_aEMeasurable
Proof state before:
case h
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 : Set X
f g : X → ℝ≥0∞
sm : MeasurableSet s
fg : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : X), x ∈ s → f x ≤ g x
Tactic:
exact ae_of_all _ fg
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
c z : Box
rs : Floating
c' z' : ℂ
rs' : ℝ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
k n : ℕ
⊢ let i := iterate' c z rs k n;
  let w' := (f' 2 c')^[i.n - k] z';
  k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
Tactic:
induction' n with n h generalizing k z z'
Proof state after:
case zero
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k 0;
  let w' := (f' 2 c')^[i.n - k] z';
  k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)

case succ
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k (n + 1);
  let w' := (f' 2 c')^[i.n - k] z';
  k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
Theorem: iterate'_correct
Proof state before:
case zero
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k 0;
  let w' := (f' 2 c')^[i.n - k] z';
  k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
Tactic:
simpa only [iterate', le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero, id_eq,
  IsEmpty.forall_iff, and_true, true_and]
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
case succ
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ let i := iterate' c z rs k (n + 1);
  let w' := (f' 2 c')^[i.n - k] z';
  k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
Tactic:
simp only [iterate', Floating.val_lt_val]
Proof state after:
case succ
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
⊢ k ≤
      (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
        else
          if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
          else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                else
                  if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                  else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).z ∧
      ((if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
            else
              if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
              else iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z.re.sqr.lo.add z.im.sqr.lo false = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < (z.re.sqr.lo.add z.im.sqr.lo false).val then { z := z, n := k, exit := Exit.large }
                        else
                          iterate' c ({ re := z.re.sqr - z.im.sqr, im := (z.re * z.im).scaleB 1 } + c) rs (k + 1) n).n -
                    k]
                z') ^
            2)
Theorem: iterate'_correct
Proof state before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
⊢ w = z.sqr + c
Tactic:
rw [←hw, Box.sqr, hzr2, hzi2]
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
⊢ f' 2 c' z' ∈ approx w
Tactic:
rw [we, f']
Proof state after:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
⊢ z' ^ 2 + c' ∈ approx (z.sqr + c)
Theorem: iterate'_correct
Proof state before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
⊢ z' ^ 2 + c' ∈ approx (z.sqr + c)
Tactic:
mono
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : z2 = nan
⊢ k ≤
      (if z2 = nan then { z := z, n := k, exit := Exit.nan }
        else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).z ∧
      ((if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < z2.val then { z := z, n := k, exit := Exit.large }
                        else iterate' c w rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
simpa only [z2n, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero,
  id_eq, IsEmpty.forall_iff, and_true, true_and]
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ k ≤
      (if z2 = nan then { z := z, n := k, exit := Exit.nan }
        else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n ∧
    (f' 2
              c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).n -
              k]
          z' ∈
        approx
          (if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).z ∧
      ((if z2 = nan then { z := z, n := k, exit := Exit.nan }
            else if rs.val < z2.val then { z := z, n := k, exit := Exit.large } else iterate' c w rs (k + 1) n).exit =
          Exit.large →
        rs' <
          Complex.abs
              ((f' 2
                    c')^[(if z2 = nan then { z := z, n := k, exit := Exit.nan }
                      else
                        if rs.val < z2.val then { z := z, n := k, exit := Exit.large }
                        else iterate' c w rs (k + 1) n).n -
                    k]
                z') ^
            2)
Tactic:
simp only [z2n, rz, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero,
  id_eq, zm, forall_true_left, true_and, Complex.abs_def,
  Real.sq_sqrt (Complex.normSq_nonneg _), if_false]
Proof state after:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ rs' < Complex.normSq z'
Theorem: iterate'_correct
Proof state before:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ rs' < Complex.normSq z'
Tactic:
refine lt_of_le_of_lt rsm (lt_of_lt_of_le rz ?_)
Proof state after:
case pos
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
h :
  ∀ {z : Box} {z' : ℂ},
    z' ∈ approx z →
      ∀ (k : ℕ),
        let i := iterate' c z rs k n;
        let w' := (f' 2 c')^[i.n - k] z';
        k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs w' ^ 2)
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : rs.val < z2.val
⊢ z2.val ≤ Complex.normSq z'