theorem proved term proof

`homogenization_limit`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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

proof body

Term-mode proof.

  50
  51end Meta
  52end IndisputableMonolith

depends on (13)

Lean names referenced from this declaration's body.

metric_det in IndisputableMonolith.Foundation.Hamiltonian decl_use
MetricTensor in IndisputableMonolith.Foundation.Hamiltonian decl_use
SimplicialLedger in IndisputableMonolith.Foundation.SimplicialLedger decl_use
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
H_HomogenizationLimit in IndisputableMonolith.Meta.Homogenization decl_use
metric_det in IndisputableMonolith.Meta.Homogenization decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
SimplicialDensity in IndisputableMonolith.Meta.Homogenization decl_use
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
metric_det in IndisputableMonolith.Relativity.Geometry.Metric decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use