Pinned Loading

1. UnbalancedHaarWavelet UnbalancedHaarWavelet Public

   This is a Lean 4 project whose goal is to formalize the construction of unbalanced Haar wavelets on measure spaces equipped with a finite measure and a sequence of finite measurable partitions.

   Lean

2. Burkholder Burkholder Public

   This repository formalizes in Lean the Burkholder martingale transform inequality, including the construction of Burkholder’s majorant function and its application to sharp Lp estimates for real-va…

   Lean

3. LaminarFamiliesMaximalBinaryTrees LaminarFamiliesMaximalBinaryTrees Public

   This Lean 4 project formalizes a mathematical structure BinaryTreeWithRootandTops, which models a rooted, ordered binary tree whose nodes are pairs of disjoint, nonempty, finite subsets of a finite…

   Lean

4. Math-Animations Math-Animations Public

   Some Python scripts that generate animations to illustrate mathematical ideas.

   Python 1 1

5. UnconditionalSchauderBasis UnconditionalSchauderBasis Public

   A Lean 4/mathlib project formalizing Schauder bases and unconditional Schauder bases for Banach spaces.

   Lean

6. Tide-Prediction Tide-Prediction Public

   Harmonic Tide Prediction-This script Illustrates harmonic tide prediction with standard Python tools. It is a non-profissional harmonic prediction tool for sea level that generates a short animation.

   Python 1