• math
  • index
  • I by descipline
  • 3 mathematics
    • 3.1 tool
    • 3.2 discipline
    • 3.3 learning map
  • 4 physics
    • 4.1 discipline
    • 4.2 learning map
  • 5 plot
  • 6 programming language
    • 6.1 discipline
    • 6.2 learning map
  • 7 machine learning
    • 7.1 Shai Ben-David
    • 7.2 deep learning
      • 7.2.1 我妻幸長
  • II by date
  • 9 A Minimal Book Example
    • 9.1 About
      • 9.1.1 Usage
      • 9.1.2 Render book
      • 9.1.3 Preview book
    • 9.2 Hello bookdown
      • 9.2.1 A section
        • An unnumbered section
    • 9.3 Cross-references
      • 9.3.1 Chapters and sub-chapters
      • 9.3.2 Captioned figures and tables
    • 9.4 Parts
    • 9.5 Footnotes and citations
      • 9.5.1 Footnotes
      • 9.5.2 Citations
    • 9.6 Blocks
      • 9.6.1 Equations
      • 9.6.2 Theorems and proofs
      • 9.6.3 Callout blocks
    • 9.7 Sharing your book
      • 9.7.1 Publishing
      • 9.7.2 404 pages
      • 9.7.3 Metadata for sharing
  • 10 test
    • 10.1 RStudio
      • 10.1.1 RMarkdown preview LaTeX equation options
      • 10.1.2 writer options
        • 10.1.2.1 line wrapping
        • 10.1.2.2 ensuring the same markdown between source / visual mode
      • 10.1.3 Rtools
      • 10.1.4 addins
      • 10.1.5 Git
    • 10.2 RMarkdown
      • 10.2.1 verbatim
      • 10.2.2 Pandoc link
      • 10.2.3 URL
      • 10.2.4 arrow
      • 10.2.5 superscript and subscript
        • 10.2.5.1 LaTeX
        • 10.2.5.2 equation
        • 10.2.5.3 aligned
        • 10.2.5.4 proof QED
      • 10.2.6 image
        • 10.2.6.1 DiagrammeR / mermaid flowchart
        • 10.2.6.2 multiple images / figures in the same line
        • 10.2.6.3 figure size
          • 10.2.6.3.1 knitr
          • 10.2.6.3.2 out.width vs. fig.width
        • 10.2.6.4 dynamic knitr plot width and height
        • 10.2.6.5 web image in PDF
        • 10.2.6.6 SVG
      • 10.2.7 horizontal rule
      • 10.2.8 footnote
      • 10.2.9 hyperlink
      • 10.2.10 code chunk
        • 10.2.10.1 code folding
      • 10.2.11 xaringan
      • 10.2.12 embed HTML or web page
        • 10.2.12.1 iframe
        • 10.2.12.2 include URL
        • 10.2.12.3 htmltools
      • 10.2.13 embed PDF
    • 10.3 Bookdown
      • 10.3.1 system locale
      • 10.3.2 render_book()
      • 10.3.3 serve_book()
      • 10.3.4 LaTeX
        • 10.3.4.1 hyperlink, URL, href
        • 10.3.4.2 ugly mathptmx \(\sum\)
        • 10.3.4.3 LaTeX package in HTML document
      • 10.3.5 depth of table of contents toc_depth
      • 10.3.6 multi-column layout / two columns
        • 10.3.6.1 for both HTML and PDF
        • 10.3.6.2 multi-column fig.cap must use fig.pos="H"
        • 10.3.6.3 caption above figure
        • 10.3.6.4 for only HTML
          • 10.3.6.4.1 CSS flex
          • 10.3.6.4.2 CSS grid
    • 10.4 conditional block/chunk for either HTML or PDF, and Chinese issue
    • 10.5 video embedding
      • 10.5.1 timestamp
    • 10.6 equation term coloring
      • 10.6.1 font color
      • 10.6.2 background color
    • 10.7 link and reference
    • 10.8 number and reference equations
    • 10.9 footnote
    • 10.10 citation
      • 10.10.1 citation in fig.cap
      • 10.10.2 backreference
    • 10.11 environment for definition, theorem, proof
      • 10.11.1 collapsible panel or HTML component
        • 10.11.1.1 nested collapsible panel or HTML component
    • 10.12 slide or presentation
      • 10.12.1 Xaringan and Infinite Moon Reader
      • 10.12.2 ioslides
      • 10.12.3 PowerPoint
  • 11 test2
  • 12 partition
  • 13 equivalence class
  • 14 equivalence relation
  • 15 Python
    • 15.1 using Python in R / RMarkdown
    • 15.2 SoloLearn
    • 15.3 list comprehension
    • 15.4 functional programming
    • 15.5 object-oriented programming = OOP
  • 16 TikZ
    • 16.1 2D
    • 16.2 3D
    • 16.3 plots of functions
    • 16.4 commutative diagram
      • 16.4.1 arrows
        • 16.4.1.1 predefined arrow tip in TikZ
          • 16.4.1.1.1 stealth arrow tip
          • 16.4.1.1.2 reversed stealth arrow tip
          • 16.4.1.1.3 to arrow tip
          • 16.4.1.1.4 latex arrow tip
          • 16.4.1.1.5 | arrow tip
        • 16.4.1.2 arrows.meta
          • 16.4.1.2.1 reversing, halving, swapping, opening
          • 16.4.1.2.2 mathematical arrows
          • 16.4.1.2.3 ray arrow tip
          • 16.4.1.2.4 arrow head scale
          • 16.4.1.2.5 arrow head size
          • 16.4.1.2.6 arrow head slant
          • 16.4.1.2.7 arrow head color
          • 16.4.1.2.8 multiple arrow head
        • 16.4.1.3 default stealth arrow
        • 16.4.1.4 harpoon
        • 16.4.1.5 bend
        • 16.4.1.6 rounded corners
        • 16.4.1.7 crossing over
        • 16.4.1.8 tweaking to paths
      • 16.4.2 label
        • 16.4.2.1 single quotation mark to swap
        • 16.4.2.2 swap
        • 16.4.2.3 every arrow swap
      • 16.4.3 box in TikZ-CD
      • 16.4.4 examples
      • 16.4.5 put a commutative diagram in a nodepart in a tikzpicture
    • 16.5 PGFplots
      • 16.5.1 the axis environments
      • 16.5.2 axis descriptions
        • 16.5.2.1 placement of axis descriptions
          • 16.5.2.1.1 coordinate system axis description cs
          • 16.5.2.1.2 legend
          • 16.5.2.1.3 tick option
      • 16.5.3 declare function
        • 16.5.3.1 pgfmathparse
        • 16.5.3.2 pgfmathdeclarefunction
      • 16.5.4 |- and -| in TikZ
      • 16.5.5 pgfplotsinvokeforeach
      • 16.5.6 interpolation dashed lines
      • 16.5.7 Zewbie
        • 16.5.7.1 coordinate axis/axes fine-tuing
          • 16.5.7.1.1 range
          • 16.5.7.1.2 scaling
          • 16.5.7.1.3 direction vector
          • 16.5.7.1.4 axis style
          • 16.5.7.1.5 axis discontinuity
          • 16.5.7.1.6 tick
        • 16.5.7.2 addplot+
        • 16.5.7.3 point
        • 16.5.7.4 line
        • 16.5.7.5 plane
        • 16.5.7.6 polar coordinate
      • 16.5.8 Arnav Bandekar: Using pgfplots to make economic graphs in LaTeX
      • 16.5.9 PGFplots gallery
    • 16.6 TikZplotLib / tikzplotlib
    • 16.7 animation
  • 17 xy-pic
    • 17.1 pure LaTeX equation environment not rendering xy-pic in HTML
    • 17.2 R figure knit with TikZ engine
  • 18 statistics
    • 18.1 Hung Hung
      • 18.1.1 probability theory
        • 18.1.1.1 probability function
        • 18.1.1.2 conditional probability
      • 18.1.2 univariable distribution
        • 18.1.2.1 cumulative distribution function
        • 18.1.2.2 probability density function
        • 18.1.2.3 range vs. support
        • 18.1.2.4 continuous monotone transformation
        • 18.1.2.5 discrete monotone transformation
        • 18.1.2.6 expected value
        • 18.1.2.7 moment
          • 18.1.2.7.1 moment generating function
          • 18.1.2.7.2 characteristic function
        • 18.1.2.8 common families of distributions
          • 18.1.2.8.1 discrete distribution
          • 18.1.2.8.2 continuous distribution
        • 18.1.2.9 exponential family
          • 18.1.2.9.1 binomial distribution with known \(n\)
          • 18.1.2.9.2 continuous uniform distribution not in exponential family
          • 18.1.2.9.3 normal distribution is in exponential family
          • 18.1.2.9.4 normal distribution with unknown equal mean and standard deviation in curved exponential family
          • 18.1.2.9.5 properties of exponential family
      • 18.1.3 multivariable distribution
    • 18.2 Chen, Lin-An
  • 19 covariance matrix
    • 19.1 vector direct product
      • 19.1.1 vector direct product: increasing rank
      • 19.1.2 vector inner product: decreasing rank
      • 19.1.3 tensor direct product: increasing rank
    • 19.2 covariance matrix and its properties
      • 19.2.1 \(\mathrm{V}\left[\boldsymbol{X}+\boldsymbol{b}\right]=\mathrm{V}\left[\boldsymbol{X}\right]\)
      • 19.2.2 \(\mathrm{V}\left[A\boldsymbol{X}\right]=A\mathrm{V}\left[\boldsymbol{X}\right]A^{\intercal}\)
      • 19.2.3 \(\mathrm{V}\left[A\boldsymbol{X}+\boldsymbol{b}\right]=A\mathrm{V}\left[\boldsymbol{X}\right]A^{\intercal}\)
  • 20 Gosper algorithm
    • 20.1 Zhuli
    • 20.2 TaylorCatAlice
  • 21 Lorentz transformation
    • 21.1 Einstein
    • 21.2 Bondi \(k\)-calculus
    • 21.3 wordline in Minkowski space
      • 21.3.1 Wick rotation
        • 21.3.1.1 Osterwalder-Schrader reconstruction theorem
  • 22 R
    • 22.1 TonyKuoYJ
      • 22.1.1 quick intro
        • 22.1.1.1 function
      • 22.1.2 R style
      • 22.1.3 data workflow or forward pipe
        • 22.1.3.1 %>% operator
      • 22.1.4 data processing with dplyr
      • 22.1.5 visualization statically with ggplot2
      • 22.1.6 loop
      • 22.1.7 variable type
        • 22.1.7.1 date
        • 22.1.7.2 time
        • 22.1.7.3 quotient %/% operator
      • 22.1.8 data type
        • 22.1.8.1 vector
          • 22.1.8.1.1 logic
          • 22.1.8.1.2 rep repeat
          • 22.1.8.1.3 seq sequence
        • 22.1.8.2 factor
        • 22.1.8.3 matrix
        • 22.1.8.4 data frame
          • 22.1.8.4.1 selecting variable or column
          • 22.1.8.4.2 filtering observation or row
          • 22.1.8.4.3 check mixed data type
    • 22.2 W3School
      • 22.2.1 same multiple variable
      • 22.2.2 legal variable name
      • 22.2.3 complex number
      • 22.2.4 escape character
      • 22.2.5 global assignment <<-
      • 22.2.6 data type
        • 22.2.6.1 array
        • 22.2.6.2 list
    • 22.3 Apan Liao
      • 22.3.1 data input
      • 22.3.2 descriptive statistics
  • 23 Laplace transform
  • 24 conic section
    • 24.1 Cartesian coordinate: focus, directrix, eccentricity
    • 24.2 two-definition equivalence for ellipse and hyperbola
      • 24.2.1 first definition for conic sections including ellipses and hyperbolas
      • 24.2.2 second definition for ellipses and hyperbolas
      • 24.2.3 eccentricity and its equivalent representation
    • 24.3 Cartesian coordinate: standard form / standard equation
    • 24.4 parametric equation
    • 24.5 polar coordinate
    • 24.6 Cartesian coordinate: general form / quadratic equation
    • 24.7 homogeneous coordinate
    • 24.8 TalyorCatAlice: projective geometry
    • 24.9 double cone
    • 24.10 theorem proof without analytic method
  • 25 distance from a point to a line
    • 25.1 by shortest \(\overline{PP^{\prime}}\)
    • 25.2 by perpendicular foot
    • 25.3 by normal vector
    • 25.4 by Cauchy inequality
  • 26 real symmetric matrix diagonalizable
  • 27 tangent half-angle formula
  • 28 homogeneous coordinate
    • 28.1 Cem Yuksel
  • 29 Archimedean property
    • 29.1 integer Archimedean property
    • 29.2 rational Archimedean property
    • 29.3 real Archimedean property
  • 30 MatPlotLib / matplotlib
    • 30.1 Timothy H. Wu
      • 30.1.1 funcitonal API
      • 30.1.2 object-oriented API
        • 30.1.2.1 Configure the figure size and DPI
        • 30.1.2.2 subplot
        • 30.1.2.3 color and linestyle
        • 30.1.2.4 other inputs
        • 30.1.2.5 legend
        • 30.1.2.6 customize style
        • 30.1.2.7 save to file
      • 30.1.3 Seaborn
        • 30.1.3.1 basic
        • 30.1.3.2 data frame
        • 30.1.3.3 axis-level plot and figure-level plot
        • 30.1.3.4 accessing fgure and axes objects
        • 30.1.3.5 distribution plot
          • 30.1.3.5.1 histogram
          • 30.1.3.5.2 ECDF = empirical cumulative distrutive function
          • 30.1.3.5.3 KDE = kernel density estimation
        • 30.1.3.6 categorical plot
        • 30.1.3.7 joint plot
        • 30.1.3.8 pair plot
        • 30.1.3.9 palette
        • 30.1.3.10 volcano plot
        • 30.1.3.11 heatmap
    • 30.2 export
      • 30.2.1 .svg
      • 30.2.2 .eps
  • 31 survial analysis
    • 31.1 Python package tableone
    • 31.2 Python package lifelines
  • 32 Manim
    • 32.1 VSCode extension: Manim Sideview
    • 32.2 installation
      • 32.2.1 Conda
    • 32.3 quickstart
  • 33 ggplot2
    • 33.1 geom
      • 33.1.1 basic plot system decomposition
    • 33.2 statistic
    • 33.3 scale
    • 33.4 coordinate system
    • 33.5 facet
    • 33.6 jitter
    • 33.7 font
  • 34 notational system for design
    • 34.1 graphic notation
    • 34.2 pre-experimental design
      • 34.2.1 one-shot case study
      • 34.2.2 one-group pretest-posttest design
      • 34.2.3 static-group comparison
    • 34.3 true experimental design
      • 34.3.1 posttest-only control group design
      • 34.3.2 pretest-posttest control group design
      • 34.3.3 Solomon four-group design
    • 34.4 quasi-experimental design
    • 34.5 correlational and ex post facto designs
    • 34.6 graphic notation, advanced
  • 35 design of experiment
    • 35.1 notational system for design[@ref(notational-system-for-design)]
    • 35.2 terminology
      • 35.2.1 replication vs. subsample
      • 35.2.2 replication vs. repeated measurements
      • 35.2.3 replication, replicate
        • 35.2.3.1 technical replicate, biological replicate
      • 35.2.4 Latin square design
      • 35.2.5 model assumption and experimental unit, measurement/observational unit
    • 35.3 experiment structure
      • 35.3.1 treatment structure
      • 35.3.2 design structure
      • 35.3.3 size of experimental unit
    • 35.4 approach to experimentation
    • 35.5 sample size estimation
    • 35.6 statistical analysis plan
    • 35.7 protocol
    • 35.8 DoE course with six sigma and Mintab
      • 35.8.1 evolution
  • 36 quine
    • 36.1 %r
  • 37 quaternion
    • 37.1 TaylorCatAlice
      • 37.1.1 complex / dionion / bionion
      • 37.1.2 trionion / triernion / triplex / ternion
      • 37.1.3 quaternion
        • 37.1.3.1 true origin of ( dot product & cross product ) / ( inner product & outer product )
        • 37.1.3.2 commutativity vs. anticommutativity
          • 37.1.3.2.1 commutativity
          • 37.1.3.2.2 anticommutativity
        • 37.1.3.3 bracket
          • 37.1.3.3.1 self-invented bracket
          • 37.1.3.3.2 Poisson bracket
          • 37.1.3.3.3 Lagrange bracket
          • 37.1.3.3.4 Lie bracket
        • 37.1.3.4 triple product
        • 37.1.3.5 differential operator
          • 37.1.3.5.1 4-differential operator
          • 37.1.3.5.2 nabla
          • 37.1.3.5.3 Laplace operator
          • 37.1.3.5.4 d’Alembert operator
        • 37.1.3.6 electromagnetism
          • 37.1.3.6.1 4-potential
          • 37.1.3.6.2 Maxwell compromise for both quaternion and 3-vector
        • 37.1.3.7 Joule heat vs. Thomson heat (Kelvin heat?)
          • 37.1.3.7.1 thermoelectric effect
        • 37.1.3.8 source term
      • 37.1.4 quaternion group
        • 37.1.4.1 2D rotation
          • 37.1.4.1.1 matrix
          • 37.1.4.1.2 complex
          • 37.1.4.1.3 \(SO\left(2\right)\cong U\left(1\right)\)
        • 37.1.4.2 3D rotation
          • 37.1.4.2.1 matrix
          • 37.1.4.2.2 quaternion
      • 37.1.5 octonion
    • 37.2 Krasjet
      • 37.2.1 Rodrigues rotation
      • 37.2.2 quaternion operation
      • 37.2.3 matrix form
      • 37.2.4 exponential form
      • 37.2.5 double cover
      • 37.2.6 right-hand vs. left-hand coordinates
        • 37.2.6.1 clock
        • 37.2.6.2 Rodrigues rotation in right-hand vs. left-hand coordinates
      • 37.2.7 gimbal lock
      • 37.2.8 Lie group
        • 37.2.8.1 Mathemaniac
        • 37.2.8.2 Liang, Can-Bin
        • 37.2.8.3 special unitary group
      • 37.2.9 geometric algebra and Clifford algebra
      • 37.2.10 dual quaternion
      • 37.2.11 interpolation
        • 37.2.11.1 Lerp
        • 37.2.11.2 Nlerp
        • 37.2.11.3 Slerp
    • 37.3 visualization
    • 37.4 3Blue1Brown
      • 37.4.1 Ben Eater
      • 37.4.2 3B1B
      • 37.4.3 Sutrabla
    • 37.5 CCJou: LA Revelation
  • 38 DICOM
    • 38.1 Innolitics: DICOM Standard Browser
    • 38.2 David Clunie: Medical Image Format Site
    • 38.3 Hsiao, Chia-Hung
  • 39 tendon pathophysiology
    • 39.1 histology
  • 40 group theory
    • 40.1 matrix group
    • 40.2 group definition and basic theorem
    • 40.3 EpicOrganism = AIRoswell = Pan, Yi-Wen
    • 40.4 PKU-CFCS
    • 40.5 Mathemaniac
    • 40.6 Polya enumeration theorem
    • 40.7 complex group representation
      • 40.7.1 complex basis group
      • 40.7.2 \(\mathbb{C}\rightarrow\mathcal{M}_{2\times2}\left(\mathbb{R}\right)\)
      • 40.7.3 ( determinant of complex group representation ) equivalent to ( squared modulus of complex number )
        • 40.7.3.1 Lagrange identity
      • 40.7.4 Euler formula proved by complex group representation
    • 40.8 quaternion group representation
      • 40.8.1 \(\mathbb{H}\rightarrow\mathcal{M}_{2\times2}\left(\mathbb{C}\right)\)
        • 40.8.1.1 Euler identity
      • 40.8.2 \(\mathbb{H}\rightarrow\mathcal{M}_{4\times4}\left(\mathbb{R}\right)\)
  • 41 tensor
    • 41.1 Einstein summation convention
      • 41.1.1 dummy index
      • 41.1.2 free index
    • 41.2 EpicOrganism = AIRoswell = Pan, Yi-Wen
    • 41.3 EigenChris
      • 41.3.1 tensor for beginner
      • 41.3.2 tensor calculus
    • 41.4 Elliot Schneider
      • 41.4.1 Fundamentals of Cartesian Tensors
      • 41.4.2 Fundamentals of Curvilinear Tensors
      • 41.4.3 Fundamentals of Spacetime Tensors
    • 41.5 Lin, Hsiu-Hau / Porcupine Lin / Hedgehog Note
  • 42 dual space
    • 42.1 linear equations
    • 42.2 matrix multiplication
    • 42.3 functional
    • 42.4 definition of linear functional
    • 42.5 set of all linear transformations is a vector space
    • 42.6 definition of dual space
    • 42.7 double dual
  • 43 vector space
    • 43.1 What is a vector?
    • 43.2 vector space definition
      • 43.2.1 commutative group structure of vector space
      • 43.2.2 scalar distributivity
    • 43.3 linearity
      • 43.3.1 linear structure of vector space
      • 43.3.2 linear transformation or linear map
    • 43.4 vector space example
      • 43.4.1 reciprocal space
        • 43.4.1.1 Kronecker delta
        • 43.4.1.2 double dual concept
    • 43.5 EpicOrganism = AIRoswell = Pan, Yi-Wen
    • 43.6 field
    • 43.7 module
    • 43.8 subspace
  • 44 \(\mathrm{d}f\)
    • 44.1 \(\mathrm{d}f\) decomposed with partials as a set of basis in vector space
    • 44.2 dual space of span of partials
    • 44.3 directional derivative
    • 44.4 coefficient of linear combination for vector space and dual space
    • 44.5 change of basis / change of coordinate
    • 44.6 ambiguity with partial notation
    • 44.7 1-form
    • 44.8 What is Math: differential geometry
    • 44.9 Liang, Can-bin: differential geometry and general relativity
  • 45 determinant
    • 45.1 induction of determinant axioms
    • 45.2 determinant axioms
    • 45.3 determinant theorems or properties
    • 45.4 ellipse area
    • 45.5 Cramer rule geometry perspective
  • 46 hypergeometric function
    • 46.1 linear space of function
    • 46.2 beta function
      • 46.2.1 Wallis product formula
    • 46.3 gamma function
    • 46.4 recursion
    • 46.5 mean and variance of discrete probability distributions
    • 46.6 CORDIC = coordinate rotation digital computer
  • 47 Feynman method
    • 47.1 Feynman method of differentiation / derivative technique
      • 47.1.1 principle
      • 47.1.2 examples
    • 47.2 Feynman method of integration / integral technique
      • 47.2.1 principle
      • 47.2.2 Dirichlet integral
        • 47.2.2.1 residue method
        • 47.2.2.2 sinc function
      • 47.2.3 Gaussian integral
      • 47.2.4 other examples
    • 47.3 Feynman method of path integral
  • 48 Hilbert space
    • 48.1 Taylor expansion or Taylor series
      • 48.1.1 Elliot Schneider: Taylor series
        • 48.1.1.1 making complicated equastion simple
        • 48.1.1.2 non-relativistic limit
        • 48.1.1.3 quantum momentum operator
    • 48.2 Dirac delta function
      • 48.2.1 complex delta function
      • 48.2.2 3D delta function
      • 48.2.3 quantum state
      • 48.2.4 rigorous definition of delta function
    • 48.3 Fourier expansion or Fourier series
      • 48.3.1 Taylor vs. Fourier
    • 48.4 Hilbert space construction
      • 48.4.1 inner product space
      • 48.4.2 Riesz representation theorem
    • 48.5 Dirac bracket
      • 48.5.1 Dirac bracket symmetry
    • 48.6 quantum operator
    • 48.7 Gram-Schmidt algorithm to find orthonormal basis
    • 48.8 Hermite polynomials and Legendre polynomials
  • 49 Lagrange inversion
    • 49.1 Newton
    • 49.2 Lagrange
  • 50 quantum color dynamics
  • 51 Lagrangian
  • 52 Hamiltonian
  • 53 Fourier analysis
    • 53.1 basic calculation
    • 53.2 TaylorCatAlice: phase velocity vs. group velocity
    • 53.3 quantum mechanics or wave mechanics
      • 53.3.1 uncertainty principle
    • 53.4 Simon Xu
      • 53.4.1 DFT = discrete Fourier transform
      • 53.4.2 FFT = fast Fourier transform
      • 53.4.3 wavelet
        • 53.4.3.1 compressed sensing MRI
    • 53.5 sampling and reconstruction
    • 53.6 signal and system
    • 53.7 image compression / data compression
    • 53.8 Lin, Chi–Kun
  • 54 axiom of choice
    • 54.1 Zorn lemma
  • 55 linear algebra
    • 55.1 The Art of Linear Algeba
    • 55.2 CCJou
      • 55.2.1 coordinate
      • 55.2.2 linear transformation
      • 55.2.3 change of basis
        • 55.2.3.1 differential polynomial
          • 55.2.3.1.1 Chebyshev polynomial
          • 55.2.3.1.2 Hermite polynomial
      • 55.2.4 singular value decomposition
    • 55.3 Chi, Chen-Yu
  • 56 analysis
    • 56.1 real analysis
    • 56.2 Chi, Chen-Yu
    • 56.3 Chen, Jin-Tzu
    • 56.4 \(\sigma\)-algebra
    • 56.5 complex anaylsis
      • 56.5.1 Mathemaniac
  • 57 matrix calculus
    • 57.1 vector-by-scalar
    • 57.2 scalar-by-vector
    • 57.3 vector-by-vector
      • 57.3.1 numerator-layout notation
      • 57.3.2 denominator-layout notation
  • 58 genetics
    • 58.1 term
    • 58.2 marker
    • 58.3 genome project
    • 58.4 linkage analysis
      • 58.4.1 PLA = parametric linkage analysis
      • 58.4.2 VCLA = variance component linkage analysis
    • 58.5 association analysis
  • 59 multivariate normal distribution
    • 59.1 bivariate normal distribution
  • 60 logic
    • 60.1 Shai Ben-David
  • 61 algorithm
    • 61.1 Chen, Vivian
    • 61.2 The Bubble Sort Curve
  • 62 computer graphics
    • 62.1 Cem Yuksel
      • 62.1.1 introduction
        • 62.1.1.1 2D transformation
          • 62.1.1.1.1 translation
          • 62.1.1.1.2 scale
          • 62.1.1.1.3 non-uniform scale
          • 62.1.1.1.4 rotation
          • 62.1.1.1.5 skew = rotation + non-uniform scale + rotation
          • 62.1.1.1.6 any \(2\times2\) matrix
          • 62.1.1.1.7 homogeneous coordinate
          • 62.1.1.1.8 position vs. direction
        • 62.1.1.2 3D transformation
          • 62.1.1.2.1 homogeneous coordinate
          • 62.1.1.2.2 scale
          • 62.1.1.2.3 translation
      • 62.1.2 interactive
  • 63 autoregression in time series
    • 63.1 AR(1) = \(1^\text{st}\)-order autoregressive model = first-order autoregressive model
    • 63.2 AR(2) = \(2^\text{nd}\)-order autoregressive model = second-order autoregressive model
    • 63.3 AR(\(p\)) = \(p^\text{th}\)-order autoregressive model
    • 63.4 MA(\(q\)) = \(q^\text{th}\)-order moving-average model
    • 63.5 ARMA(\(p\),\(q\)) = \(p^\text{th},q^\text{th}\)-order autoregressive-moving-average model
  • 64 conductivity
    • 64.1 resistance
    • 64.2 semiconductor
  • 65 LaTeX annotation by TikZ
  • 66 Shannon sampling
  • 67 brachistochrone
  • 68 magnetic resonance
    • 68.1 NMR
      • 68.1.1 Bloch equation
      • 68.1.2 Bloch-Torrey equation
    • 68.2 MRI
      • 68.2.1 Lin, Hsiu-Hau
      • 68.2.2 MRI: Physics and Image Creation
      • 68.2.3 Tseng, Wen-Yih Isaac
  • 69 OpenMMLab
    • 69.1 Tongji TommyZihao
    • 69.2 official
  • 70 linear programming
    • 70.1 simplex method
    • 70.2 duality method
    • 70.3 integer linear programming
  • 71 TaylorCatAlice physics
    • 71.1 dimensional analysis
    • 71.2 classic mechanics
      • 71.2.1 Galileo
      • 71.2.2 Newton
      • 71.2.3 Lagrange
      • 71.2.4 Hamilton
    • 71.3 electromagnetism
    • 71.4 relativity
    • 71.5 quantum theory
      • 71.5.1 old quantum theory
      • 71.5.2 black-body radiation
      • 71.5.3 quantum mechanics
        • 71.5.3.1 Heisenberg: matrix mechanics
        • 71.5.3.2 Schrodinger: wave mechanics
        • 71.5.3.3 Dirac: relativistic quantum mechanics
          • 71.5.3.3.1 spin
        • 71.5.3.4 other
      • 71.5.4 resistance and conductivity
  • 72 fundamental theorem of algebra
    • 72.1 Gauss
      • 72.1.1 FToA
      • 72.1.2 trial and error
      • 72.1.3 heptadecagon
    • 72.2 equation
      • 72.2.1 cubic equation
      • 72.2.2 qunitic equation
  • 73 Basel problem
    • 73.1 TaylorCatAlice
    • 73.2 3B1B
    • 73.3 Riemann hypothesis
  • 74 number theory
    • 74.1 4 important theorems
    • 74.2 congruence modulo
  • 75 spinor
    • 75.1 EigenChris
    • 75.2 Shinonome Masaki
  • 76 singular value decomposition
    • 76.1 Visual Kernel
    • 76.2 CCJou: LA Revelation
  • 77 support vector machine
    • 77.1 Visually Explained
  • 78 principal component analysis
    • 78.1 Visually Explained
    • 78.2 dimension reduction: PCA, tSNE, UMAP
  • 79 transformer
    • 79.1 Lee, Hung-Yi
    • 79.2 3B1B
  • 80 differential equation
    • 80.1 ODE = ordinary DE = ordinary differential equation
      • 80.1.1 Sturm-Liouville theory
    • 80.2 PDE = partial DE = partial differential equation
  • 81 Shannon
    • 81.1 entropy
  • 82 LEAN
    • 82.1 LEAN 4
      • 82.1.1 type theory
      • 82.1.2 installation
    • 82.2 ELAN
    • 82.3 MathLib = mathlib
      • 82.3.1 yugu233 / Crispher : MathLibExplorer
    • 82.4 LEAN game server
      • 82.4.1 A LEAN Intro to Logic
      • 82.4.2 1.2.1.2 Set Theory Game
      • 82.4.3 Natural Number Game
        • 82.4.3.1 Natural Number Game in LEAN 4
    • 82.5 LEAN 4 proof tutorial
  • 83 recreational math
    • 83.1 solved
      • 83.1.1 Monty Hall problem
      • 83.1.2 goat grazing problem
    • 83.2 not yet solved
      • 83.2.1 moving sofa problem
  • 84 causal inference
  • 85 Einstein-de Hass effect
  • 86 pythagorean theorem
    • 86.1 2023 new proof with trigonometry
  • 87 general relativity
    • 87.1 EpicOrganism = AIRoswell = Pan, Yi-Wen
    • 87.2 Elliot Schneider
  • 88 LaTeX RegEx
  • 89 operator theory
  • 90 physics monsters
  • 91 List of Theorem
  • 92 Galois theory
  • 93 Sage
  • references
  • Published with bookdown

math

Chapter 82: LEAN

\(\mathrm{L}\exists\forall\mathrm{N}\) = LEAN

82.1 LEAN 4

https://en.wikipedia.org/wiki/Lean_(proof_assistant)

https://leanprover-community.github.io/

https://lean-lang.org/

82.1.1 type theory

https://www.bilibili.com/video/BV12m4y1x7CA

82.1.2 installation

https://space.bilibili.com/520713026/channel/collectiondetail?sid=2671954

82.2 ELAN

LEAN version control

82.3 MathLib = mathlib

library of LEAN theorems

https://leanprover-community.github.io/mathlib-overview.html

https://leanprover-community.github.io/mathlib4_docs/

82.3.1 yugu233 / Crispher : MathLibExplorer

https://github.com/Crispher/MathlibExplorer

https://www.bilibili.com/video/BV1Hw4m1q7qP

MathLibExplorer
MathLibExplorer

82.4 LEAN game server

https://adam.math.hhu.de/#/

82.4.1 A LEAN Intro to Logic

https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic

82.4.2 1.2.1.2 Set Theory Game

https://adam.math.hhu.de/#/g/djvelleman/stg4

82.4.3 Natural Number Game

https://adam.math.hhu.de/#/g/leanprover-community/NNG4

82.4.3.1 Natural Number Game in LEAN 4

https://www.youtube.com/playlist?list=PLCaPonEDDnrkDQVfxWiYdF0tYOYRyLI3N

https://www.youtube.com/watch?v=u_0jWOlDoPw&list=PLCaPonEDDnrkDQVfxWiYdF0tYOYRyLI3N&t=8m42s

82.5 LEAN 4 proof tutorial

https://www.youtube.com/watch?v=7Ko3QZx4saU