def
definition
H_HomogenizationLimit
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Meta.Homogenization on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
scale -
mu -
of -
metric_det -
MetricTensor -
of -
from -
SimplicialLedger -
of -
MetricTensor -
of -
metric_det -
MetricTensor -
SimplicialDensity -
volume -
density -
L -
L -
metric_det -
MetricTensor -
Metric
used by
formal source
35 on simplicial complexes.
36 FALSIFIER: Discovery of a simplicial ledger covering that does not satisfy
37 the homogenization limit. -/
38def H_HomogenizationLimit (L : SimplicialLedger) (g : MetricTensor) : Prop :=
39 ∀ ε > 0, ∃ ell0_max > 0,
40 (∀ simplex ∈ L.simplices, simplex.volume < ell0_max) →
41 ∀ x, abs (SimplicialDensity L x - Real.sqrt (abs (metric_det g (fun i => if i.val = 0 then 0 else x i)))) < ε
42
43/-- **THEOREM: Metric from Density (Homogenization)**
44 As the simplicial scale $\ell_0 \to 0$, the simplicial recognition density
45 converges to the volume form of the macroscopic metric $g_{\mu\nu}$. -/
46theorem homogenization_limit (h : H_HomogenizationLimit L g) (L : SimplicialLedger) (g : MetricTensor) :
47 ∀ ε > 0, ∃ ell0_max > 0,
48 (∀ simplex ∈ L.simplices, simplex.volume < ell0_max) →
49 ∀ x, abs (SimplicialDensity L x - Real.sqrt (abs (metric_det g (fun i => if i.val = 0 then 0 else x i)))) < ε := h
50
51end Meta
52end IndisputableMonolith