Documentation

LeanPool.NandakumarRamanaRao.NRR.EMP.VariableBody.Basic

NRR.EMP.VariableBody.Basic — variable-body power-diagram vocabulary #

This module opens the variable-body layer of the Akopyan–Avvakumov–Karasev power-partition development. A parameter is a positive-area subbody C : BodySpace K A of a fixed planar parent K, together with a configuration s : Config n and a weight vector w : Fin n → ℝ.

Every declaration here is a thin wrapper that specializes the existing fixed-body power-diagram and normalized-weight APIs to the solid body C.toGeometryConvexBody hA. No new power diagram, configuration space, weight selection, or convex-body topology is introduced.

source
noncomputable def NRR.EMP.VariableBody.solidBody {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
Geometry.ConvexBody Geometry.Plane

The solid body of a positive-area subbody parameter: the fixed-body geometry body obtained from C : BodySpace K A via the positive-area body bridge.

Equations
Instances For
    source
    def NRR.EMP.VariableBody.cellSet {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
    Set Geometry.Plane

    The restricted power cell of site i inside the variable body C, as a set.

    Equations
    Instances For
      source
      noncomputable def NRR.EMP.VariableBody.cellArea {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
      ℝ

      The area of the restricted power cell of site i inside the variable body C.

      Equations
      Instances For
        source
        def NRR.EMP.VariableBody.IsEqualAreaWeight {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) :
        Prop

        w is an equal-area weight for the sites s inside the variable body C: every restricted power cell has the average area C.area / n.

        Equations
        Instances For
          source
          def NRR.EMP.VariableBody.IsNormalizedEqualAreaWeight {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) :
          Prop

          w is a normalized equal-area weight: equal-area for s in C and normalized (∑ i, w i = 0).

          Equations
          Instances For
            source
            noncomputable def NRR.EMP.VariableBody.normalizedWeight {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (hn : 0 < n) (C : BodySpace K A) (s : Config n) :
            Fin n → ℝ

            The canonical normalized equal-area weight for the sites s inside the variable body C, selected by the fixed-body existence/uniqueness core applied to solidBody hA C.

            Equations
            Instances For
              source
              @[simp]
              theorem NRR.EMP.VariableBody.solidBody_carrier {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
              (solidBody hA C).carrier = ↑C.body.body
              source
              @[simp]
              theorem NRR.EMP.VariableBody.solidBody_area {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
              (solidBody hA C).area = C.body.area
              source
              @[simp]
              theorem NRR.EMP.VariableBody.cellSet_def {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              cellSet hA C s w i = PowerDiagram.bodyCellSet (solidBody hA C) s.pts w i
              source
              @[simp]
              theorem NRR.EMP.VariableBody.cellArea_def {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              cellArea hA C s w i = PowerDiagram.bodyCellArea (solidBody hA C) s.pts w i
              source
              theorem NRR.EMP.VariableBody.cellSet_subset_body {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              cellSet hA C s w i ⊆ ↑C.body.body
              source
              theorem NRR.EMP.VariableBody.cellSet_subset_parent {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              cellSet hA C s w i ⊆ K.carrier
              source
              theorem NRR.EMP.VariableBody.cellSet_convex {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              Convex ℝ (cellSet hA C s w i)
              source
              theorem NRR.EMP.VariableBody.cellSet_isCompact {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) :
              IsCompact (cellSet hA C s w i)
              source
              theorem NRR.EMP.VariableBody.normalizedWeight_isEqualArea {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (hn : 0 < n) (C : BodySpace K A) (s : Config n) :
              IsEqualAreaWeight hA C s (normalizedWeight hA hn C s)
              source
              theorem NRR.EMP.VariableBody.normalizedWeight_normalized {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (hn : 0 < n) (C : BodySpace K A) (s : Config n) :
              WeightNormalized (normalizedWeight hA hn C s)
              source
              theorem NRR.EMP.VariableBody.normalizedWeight_unique {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (hn : 0 < n) (C : BodySpace K A) (s : Config n) {w : Fin n → ℝ} (hw : IsNormalizedEqualAreaWeight hA C s w) :
              w = normalizedWeight hA hn C s