Talk about the convergence of the sum of $\sum_{n=1}^{\infinity} \frac{sin(anx)}{x}$

More information can be found here: A Chinese Platform: How to prove \(sin(x) < x\) regiously? Math.stackexchange: Sine inequality: How to prove that \(|sin(𝑥)|≤|𝑥|\)

Metric in L^p This is a note for proof of \[ \left[ \int _{a}^{b}\left| f\left( x\right) \right| ^{p}dx\right]^{\frac{1}{p}} \] is a norm of \(L^p\) space. Here is the structure of the whole proof (se

Explained proof of an exercise question

Bug of operator precedence in C

WebSocket Latency issues with REAL WORLD SITUATION & SOLUTION

Introduction on concept of WebSocket

Import LEAN into elan Notice: I will use lean v3.42.1 for the demonstration This is a tutorial on how to override/import LEAN into elan, so that you can regulate different versions of LEAN with a ve

Installing LEAN on arm based Mac — Manually compile and install This is a tutorial on how to compile LEAN from source code and install it. Next, we will see how to move it to elan (next post) Problem

Apple's M1 chips have ushered in a new era of computing performance. But with new architectures come new challenges. One such challenge I recently faced was setting up the Lean theorem prover. Here's