---

Step * 1 of Lemma real-ball-slice_wf


1. r : {r:ℝ| r0 ≤ r} 
2. n : ℕ+
3. t : {t:ℝ| t ∈ [-(r), r]} 
4. i : ℕn
5. p : ℝ^n - 1
6. ||p|| ≤ ball-slice-radius(r;t)
7. λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi  ∈ ℝ^n
8. (p⋅p + t^2) ≤ r^2
⊢ λj.if j <z i then p j
     if i <z j then p (j - 1)
     else t
     fi ⋅λj.if j <z i then p j
            if i <z j then p (j - 1)
            else t
            fi  ≤ r^2
BY
{ ((RWO "-1<" 0 THENA Auto)
   THEN (BLemma `rleq_weakening` THENA Auto)
   THEN D 3
   THEN ThinVar `r'
   THEN (InstLemma `dot-product-split` [⌜n⌝;⌜i⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0
         THENA (Try (QuickAuto)
                THEN RepeatFor 2 (MemCD)
                THEN Reduce 0
                THEN Try (QuickAuto)
                THEN All (Unfold `real-vec`)
                THEN Auto)
         )) }

1
1. n : ℕ+
2. t : ℝ
3. i : ℕn
4. p : ℝ^n - 1
5. λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi  ∈ ℝ^n
6. ∀[x,y:ℝ^n].  (x⋅y = (x⋅y + λi@0.(x (i + i@0))⋅λi@0.(y (i + i@0))))
⊢ (λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi ⋅λj.if j <z i then p j
             if i <z j then p (j - 1)
             else t
             fi 
+ λi@0.((λj.if j <z i then p j if i <z j then p (j - 1) else t fi ) (i + i@0))⋅λi@0.((λj.if j <z i then p j
                                                                                         if i <z j then p (j - 1)
                                                                                         else t
                                                                                         fi ) 
                                                                                     (i + i@0)))
= (p⋅p + t^2)

---

Latex:

---

Latex:

1.  r  :  \{r:\mBbbR{}|  r0  \mleq{}  r\} 
2.  n  :  \mBbbN{}\msupplus{}
3.  t  :  \{t:\mBbbR{}|  t  \mmember{}  [-(r),  r]\} 
4.  i  :  \mBbbN{}n
5.  p  :  \mBbbR{}\^{}n  -  1
6.  ||p||  \mleq{}  ball-slice-radius(r;t)
7.  \mlambda{}j.if  j  <z  i  then  p  j
            if  i  <z  j  then  p  (j  -  1)
            else  t
            fi    \mmember{}  \mBbbR{}\^{}n
8.  (p\mcdot{}p  +  t\^{}2)  \mleq{}  r\^{}2
\mvdash{}  \mlambda{}j.if  j  <z  i  then  p  j
          if  i  <z  j  then  p  (j  -  1)
          else  t
          fi  \mcdot{}\mlambda{}j.if  j  <z  i  then  p  j
                        if  i  <z  j  then  p  (j  -  1)
                        else  t
                        fi    \mleq{}  r\^{}2


By

---

Latex:
((RWO  "-1<"  0  THENA  Auto)
  THEN  (BLemma  `rleq\_weakening`  THENA  Auto)
  THEN  D  3
  THEN  ThinVar  `r'
  THEN  (InstLemma  `dot-product-split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0
              THENA  (Try  (QuickAuto)
                            THEN  RepeatFor  2  (MemCD)
                            THEN  Reduce  0
                            THEN  Try  (QuickAuto)
                            THEN  All  (Unfold  `real-vec`)
                            THEN  Auto)
              ))

---

Home Index