levels of abstractions

• 10 June 2025
• Mathematics,
• Process book,
• Learning

levels of abstraction #

I am stuck at 1 ⟶ ℝ

v₀.₀₀₁:   𝟏 ⟶ ℝ   ≡ constant f(x) = c  
v₀.₀₁:    Aff(ℝ) ⊂ Poly₁  
v₀.₁:     Polyₙ ≅ Free[ℝ[x]]  
v₁:       Tₙ(x) ∈ span{sin(nx), cos(nx)}  
v₂:       Sₙ(f) = ∑ aₖ e^{ikx} (Fourier sums)  
v₃:       Dₙ ∗ f = convolution via Dirichlet kernel  
v₄:       ∥Dₙ ∗ f − f∥_∞ → 0 : uniform convergence  
v₅:       ∥⋅∥_{Lᵖ} : approximation in norm  
v₆:       f ∈ C^k, L^p ⟶ f ≈ Poly via Stone–Weierstrass  

film is mathematics #

Set ⇄ Vct Pp ⇒ De

generatori relaxioni per costruire gruppi e categorie film custriti da motivi ricorrenti, simboli, dualita

surrealismo come funzioni non-lineari

vedere schemi astratti, analoghi a trovare simmetrie in geometria o recorrenze in algebra

built-in continuity #

via internal logci $\mathbf{Cont}(ℝ, ℝ)$ is a morphism object function space is internalised

mass-energy bends the rubber sheet

mem : {o,*} × {o,*} ⟶ Prop ~ a ∈ B is a relation b/w 2 sets 💡

(•‿•) für Kategorien, (⇨‿⇨) für Funktoren, (⌒‿⌒) für Naturtransformationen

(Hom : Obj ⟶ Obj ⟶ Type)

alogirhtms are constructive proofs of ∃ !

• in a type system Algorithm : A ⟶ B ~ Proof of (A ⇒ B)

def id (a : \a) : \a := a

∀α, α ⟶ α id_α : α ⟶ α, id_α(a) = a

id : A ⟶ B id : α ⟶ α, a ∈ α, a ⟼ a

{x // P x} is a Sigma type!

any Type defines an initial algebra to a functor different ways of writing in Lean, awesome, I learnt arrow notation is much more readable for me

equations, inequalities, basic ml stms complex stms in lean, are built u(∧∨⇒¬...∃∀)

succ(a) + b = succ(a +b) σa + b = σ(a + b)

I thought this cobordism looked like pants #

and then yesterday I learnt they are indeed called pants!

• Previous: I can be computer agent