Revision #1238 → #1721 · back to history
modifiedFractal scaling by non-integer power8c1fb164c0e2
| Field | From #1238 | To #1721 |
|---|
| note | `hausdorffMeasure_smul₀` proves μH[d](r•s)=‖r‖^d•μH[d] s for real d, formalizing how d-dimensional content scales by a possibly non-integer power, but without the 'fractal' framing. | `hausdorffMeasure_smul₀` proves μH[d](r•s)=‖r‖^d•μH[d] s for real d, formalizing how d-dimensional content scales by a possibly non-integer power, without the 'fractal' framing. |
modifiedFractal dimensionf809af8256c7
| Field | From #1238 | To #1721 |
|---|
| mathlib.decl | MeasureTheory.dimH | dimH |
| note | `MeasureTheory.dimH` is the Hausdorff dimension, the rigorous form of the fractal/scaling dimension defined for arbitrary sets. | `dimH` is the Hausdorff dimension, the rigorous form of the fractal/scaling dimension defined for arbitrary sets in an (e)metric space. |
modifiedMandelbrot 1982 definition83876923ae70
| Field | From #1238 | To #1721 |
|---|
| mathlib.decl | MeasureTheory.dimH | dimH |
modifiedRep-tiling of a squarec397142bc27c
| Field | From #1238 | To #1721 |
|---|
| mathlib.decl | MeasureTheory.dimH_univ_eq_finrank | Real.dimH_univ_eq_finrank |
| note | A square's dimension being 2 follows from `dimH_univ_eq_finrank` (and area scales by r² via `hausdorffMeasure_smul₀`), but rep-tiling is not formalized. | A square's dimension being 2 follows from `Real.dimH_univ_eq_finrank` (and area scales by r² via `hausdorffMeasure_smul₀`), but rep-tiling is not formalized. |
modifiedRep-tiling rule for n-dimensional objects8a3adce7e68b
| Field | From #1238 | To #1721 |
|---|
| note | The scaling law μH[n](r•s)=r^n·μH[n] s captures the n-dimensional scaling content, but the rep-tiling/piece-counting formulation is absent. | The scaling law μH[n](r•s)=‖r‖^n·μH[n] s captures the n-dimensional scaling content, but the rep-tiling/piece-counting formulation is absent. |
modifiedFractal dimension of the Koch curveac6e362fde2f
| Field | From #1238 | To #1721 |
|---|
| note | The Koch curve and its Hausdorff dimension log 4/log 3 are not formalized (Snowflaking.lean only mentions the Koch snowflake in prose). | The Koch curve and its Hausdorff dimension log 4/log 3 are not formalized in Mathlib. |
modifiedWeierstrass function7ba90a9ff3a1
| Field | From #1238 | To #1721 |
|---|
| note | A continuous-everywhere, nowhere-differentiable Weierstrass function is fully formalized, though it lives in the Counterexamples directory rather than the core Mathlib library. | A continuous-everywhere, nowhere-differentiable Weierstrass-type function is formalized, though it lives in the Counterexamples directory rather than core Mathlib. |
modifiedCantor sets61202df29c0a
| Field | From #1238 | To #1721 |
|---|
| note | `cantorSet` is the ternary Cantor set defined as ⋂ₙ preCantorSet n on the real line. | `cantorSet` is the ternary Cantor set defined on the real line in `Mathlib.Topology.Instances.CantorSet`. |
modifiedNon-integer (Hausdorff) dimension2b053f356136
| Field | From #1238 | To #1721 |
|---|
| mathlib.decl | MeasureTheory.dimH | dimH |
| note | `MeasureTheory.dimH` takes values in ℝ≥0∞ and may be non-integer, exactly the Hausdorff dimension allowing fractional dimensions. | `dimH` takes values in ℝ≥0∞ and may be non-integer, exactly the Hausdorff dimension allowing fractional dimensions. |
modifiedHausdorff–Besicovitch dimension exceeds topologicala39b2cc55465
| Field | From #1238 | To #1721 |
|---|
| mathlib.decl | MeasureTheory.dimH | dimH |
| note | Both `dimH` and a topological (`smallInductiveDimension`) dimension exist, but Mathlib has no predicate for dimH exceeding topological dimension. | Both `dimH` and a topological dimension (`smallInductiveDimension`) exist, but Mathlib has no predicate for dimH exceeding topological dimension. |
addedMandelbrot setb3673e77950e
addedMenger sponge2e18fa0d753c
addedTopological dimensionf9e75904b3b4
addedHausdorff dimension links fractals to measure theoryc20614388e22
addedSierpiński triangle162dd5ba8c11
addedSierpinski carpet0be9e975a60e
addedBrownian motion / Wiener process72bd59b06445
addedJulia setd6d0b0e0f18e