FacetConnectivity.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Connectivity of finite closed covers and active-cell intersection graphs.

def OAI.Problem358.closedCoverGraph line 15
Source documentation
Distinct cover members are adjacent when they meet.
```
def closedCoverGraph (s : ι → Set X) : SimpleGraph ι where
…
```
theorem OAI.Problem358.closedCoverGraph_reachable line 26
Source documentation
Any two nonempty members of a finite closed cover of a preconnected set are joined by a chain of nonempty intersections. Empty cover members are harmless.
```
theorem closedCoverGraph_reachable (s : ι → Set X)
    (hclosed : ∀ i, IsClosed (s i)) (hconn : IsPreconnected (⋃ i, s i))
    (i j : ι) (hi : (s i).Nonempty) (hj : (s j).Nonempty) :
    (closedCoverGraph s).Reachable i j := by
…
```
Mentions: OAI.Problem358.closedCoverGraph
theorem OAI.Problem358.closedCoverGraph_connected line 62
Source documentation
A finite closed cover of a preconnected set has connected intersection graph, provided every member of the cover is nonempty.
```
theorem closedCoverGraph_connected [Nonempty ι] (s : ι → Set X)
    (hclosed : ∀ i, IsClosed (s i)) (hne : ∀ i, (s i).Nonempty)
    (hconn : IsPreconnected (⋃ i, s i)) : (closedCoverGraph s).Connected :=
…
```
Mentions: OAI.Problem358.closedCoverGraph
def OAI.Problem358.ClosedCoverConnectivity.maximalCell line 70
Source documentation
The closed weak-maximizer cell of a continuous finite family.
```
def maximalCell (K : Set X) (f : ι → X → ℝ) (i : ι) : Set X :=
…
```
lemma OAI.Problem358.ClosedCoverConnectivity.maximalCell_isClosed line 74
lemma OAI.Problem358.ClosedCoverConnectivity.iUnion_maximalCell line 84
theorem OAI.Problem358.ClosedCoverConnectivity.maximalCell_graph_connected line 100
Source documentation
The nonempty affine-max cells have a connected intersection graph. This statement concerns nonempty intersections, not positive-area common facets.
```
theorem maximalCell_graph_connected [Nonempty ι] (K : Set X)
    (hclosed : IsClosed K) (hconnected : IsPreconnected K)
    (f : ι → X → ℝ) (hf : ∀ i, Continuous (f i))
    (hactive : ∀ i, (maximalCell K f i).Nonempty) :
    (closedCoverGraph (maximalCell K f)).Connected := by
…
```
Mentions: OAI.Problem358.ClosedCoverConnectivity.maximalCell, OAI.Problem358.closedCoverGraph

theorem OAI.Problem358.measure_face_pos_of_strict_tie line 124

Source documentation

A persistent tie which strictly dominates every other score is a positive measure face whenever the parameter point maps into the interior of the source. Only topology and positivity of nonempty open sets are needed.

theorem measure_face_pos_of_strict_tie
    {X W ι : Type*} [TopologicalSpace X] [TopologicalSpace W]
    [MeasurableSpace W] [Finite ι]
    (μ : Measure W) [Measure.IsOpenPosMeasure μ]
    (φ : W → X) (hφ : Continuous φ) (score : ι → X → ℝ)
    (hs : ∀ k, Continuous (score k)) (K : Set X) (z : W) (i j : ι)
    (hz : φ z ∈ interior K)
    (htie : ∀ w, score i (φ w) = score j (φ w))
    (hstrict : ∀ k, k ≠ i → k ≠ j → score k (φ z) < score i (φ z)) :
    0 < μ {w | φ w ∈ K ∧ score i (φ w) = score j (φ w) ∧
      ∀ k, score k (φ w) ≤ score i (φ w)} := by
…

theorem OAI.Problem358.affine_pair_face_surface_pos line 163

Source documentation

A two-site strict tie in the interior has positive surface measure in the tangent hyperplane of the two affine scores. No ambient volume assertion is made: the measure is intrinsically on the tangent subspace.

theorem affine_pair_face_surface_pos
    {V ι : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MeasurableSpace V] [BorelSpace V] [Finite ι]
    (y : ι → V) (c : ι → ℝ) (i j : ι) (x : V) (K : Set V)
    (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [Measure.IsOpenPosMeasure μ]
    (hx : x ∈ interior K)
    (htie : ⟪y i, x⟫_ℝ + c i = ⟪y j, x⟫_ℝ + c j)
    (hstrict : ∀ k, k ≠ i → k ≠ j →
      ⟪y k, x⟫_ℝ + c k < ⟪y i, x⟫_ℝ + c i) :
    0 < μ {w | x + (w : V) ∈ K ∧
      ⟪y i, x + (w : V)⟫_ℝ + c i = ⟪y j, x + (w : V)⟫_ℝ + c j ∧
      ∀ k, ⟪y k, x + (w : V)⟫_ℝ + c k ≤ ⟪y i, x + (w : V)⟫_ℝ + c i} := by
…

def OAI.Problem358.PositiveFacet.strictTieGraph line 204
Source documentation
Edges are interior ties with no third maximizing branch. For affine families these are precisely the local witnesses of positive-area facets.
```
def strictTieGraph (K : Set V) (f : ι → V → ℝ) : SimpleGraph ι where
…
```

theorem OAI.Problem358.PositiveFacet.strictTieGraph_reachable_of_parametric line 216

Source documentation

A connected closed parameter domain without triple ties generates a chain of strict two-cell interfaces between any two active endpoint labels. Empty cells on this particular path do not cause an obstruction.

theorem strictTieGraph_reachable_of_parametric
    (K : Set V) (f : ι → V → ℝ) (hf : ∀ i, Continuous (f i))
    (s : Set W) (hs : IsClosed s) (hconn : IsPreconnected s)
    (a : W → V) (ha : Continuous a)
    (hK : ∀ t ∈ s, a t ∈ interior K)
    (htriple : ∀ t ∈ s, ∀ i j k, i ≠ j → k ≠ i → k ≠ j →
      f i (a t) = f j (a t) → f i (a t) ≠ f k (a t))
    (i j : ι) (ti tj : W) (hti : ti ∈ s) (htj : tj ∈ s)
    (hi : ∀ k, f k (a ti) ≤ f i (a ti))
    (hj : ∀ k, f k (a tj) ≤ f j (a tj)) :
    (strictTieGraph K f).Reachable i j := by
…

Mentions: OAI.Problem358.PositiveFacet.strictTieGraph

lemma OAI.Problem358.PositiveFacet.score_difference line 261
theorem OAI.Problem358.PositiveFacet.affine_strictTieGraph_connected line 271
Source documentation
Every strictly active affine label is connected to every other by interior two-cell ties. The proof chooses an actual generic segment avoiding all triple ties, then applies finite closed-cover connectivity along that segment.
```
theorem affine_strictTieGraph_connected
    (μ : Measure E) [IsAddHaarMeasure μ]
    (K : Set E) (hK : Convex ℝ K) (y : ι → E) (c : ι → ℝ)
    (hactive : ∀ i, ∃ x ∈ interior K, ∀ j, j ≠ i →
      TripleCell.score (y j) (c j) x < TripleCell.score (y i) (c i) x) :
    (strictTieGraph K (fun i => TripleCell.score (y i) (c i))).Connected := by
…
```
Mentions: OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.strictTieGraph
def OAI.Problem358.PositiveFacet.surfaceFace line 379
Source documentation
The surface face in a tie hyperplane, translated from an arbitrary point of that plane. This is an intrinsic measure domain, not ambient volume.
```
def surfaceFace (K : Set E) (y : ι → E) (c : ι → ℝ) (i j : ι) (base : E) :
    Set ((ℝ ∙ (y i - y j))ᗮ) :=
…
```
theorem OAI.Problem358.PositiveFacet.strictTieGraph_adj_surfaceFace_pos line 391
Source documentation
Strict-facet edges have positive surface measure in a parametrization at any point of their tie plane. This transfers the local strict-face theorem to the fixed bases used when defining geometric graph coefficients.
```
theorem strictTieGraph_adj_surfaceFace_pos
    (K : Set E) (y : ι → E) (c : ι → ℝ) {i j : ι}
    (hedge : (strictTieGraph K (fun k => TripleCell.score (y k) (c k))).Adj i j)
    (base : E)
    (hbase : TripleCell.score (y i) (c i) base = TripleCell.score (y j) (c j) base)
    (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [IsOpenPosMeasure μ] :
    0 < μ (surfaceFace K y c i j base) := by
…
```
Mentions: OAI.Problem358.PositiveFacet.strictTieGraph, OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.exists_connected_positive_surface_graph line 425

Source documentation

The geometric strict-facet graph is connected and each of its edges has positive intrinsic face measure, uniformly over arbitrary tie-plane bases. No quantitative lower bound on individual face areas is needed.

theorem exists_connected_positive_surface_graph
    [FiniteDimensional ℝ E] [Nonempty ι]
    (ρ : Measure E) [IsAddHaarMeasure ρ]
    (K : Set E) (hK : Convex ℝ K) (y : ι → E) (c : ι → ℝ)
    (hactive : ∀ i, ∃ x ∈ interior K, ∀ j, j ≠ i →
      TripleCell.score (y j) (c j) x < TripleCell.score (y i) (c i) x) :
    ∃ G : SimpleGraph ι, G.Connected ∧ ∀ i j, G.Adj i j →
      ∀ base : E,
      TripleCell.score (y i) (c i) base = TripleCell.score (y j) (c j) base →
      ∀ μ : Measure ((ℝ ∙ (y i - y j))ᗮ), IsOpenPosMeasure μ →
        0 < μ (surfaceFace K y c i j base) := by
…

Mentions: OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.surfaceFace_eq_preimage_closedCells line 460

Source documentation

The intrinsic face domain is exactly the pullback of the intersection of the two canonical closed cells.

theorem surfaceFace_eq_preimage_closedCells
    (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i j : ι) (base : E d) :
    surfaceFace K y c i j base =
      (fun w : (ℝ ∙ (y i - y j))ᗮ => base + (w : E d)) ⁻¹'
        (CellGeometry.closedCell K y c i ∩ CellGeometry.closedCell K y c j) := by
…

Mentions: OAI.Problem358.PositiveFacet.surfaceFace, OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.PositiveFacet.isCompact_surfaceFace line 477
Source documentation
Compact source cells give compact surface domains in every translated tangent-plane parametrization.
```
theorem isCompact_surfaceFace
    (K : Set (E d)) (hK : IsCompact K) (y : ι → E d) (c : ι → ℝ)
    (i j : ι) (base : E d) : IsCompact (surfaceFace K y c i j base) := by
…
```
Mentions: OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.strictTieGraph_adj_surfaceFace_real_pos line 491

Source documentation

Positivity remains genuine after ENNReal.toReal: compactness excludes an infinite surface measure from being silently converted to zero.

theorem strictTieGraph_adj_surfaceFace_real_pos
    (K : Set (E d)) (hK : IsCompact K) (y : ι → E d) (c : ι → ℝ) {i j : ι}
    (hedge : (strictTieGraph K (fun k => TripleCell.score (y k) (c k))).Adj i j)
    (base : E d)
    (hbase : TripleCell.score (y i) (c i) base = TripleCell.score (y j) (c j) base)
    (μ : Measure ((ℝ ∙ (y i - y j))ᗮ))
    [IsOpenPosMeasure μ] [IsFiniteMeasureOnCompacts μ] :
    0 < (μ (surfaceFace K y c i j base)).toReal := by
…

Mentions: OAI.Problem358.PositiveFacet.strictTieGraph, OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.strictTieGraph_adj_normalized_surface_pos line 505

Source documentation

The coefficient used in the cell Laplacian is positive on every strict facet edge. Both the source-volume and surface-area toReal conversions are justified by compactness.

theorem strictTieGraph_adj_normalized_surface_pos
    (K : Set (E d)) (hK : IsCompact K) (hvol : volume K ≠ 0)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) {i j : ι}
    (hedge : (strictTieGraph K (fun k => TripleCell.score (y k) (c k))).Adj i j)
    (base : E d)
    (hbase : TripleCell.score (y i) (c i) base = TripleCell.score (y j) (c j) base)
    (μ : Measure ((ℝ ∙ (y i - y j))ᗮ))
    [IsOpenPosMeasure μ] [IsFiniteMeasureOnCompacts μ] :
    0 < (μ (surfaceFace K y c i j base)).toReal /
      ((volume K).toReal * ‖y i - y j‖) := by
…

Mentions: OAI.Problem358.PositiveFacet.strictTieGraph, OAI.Problem358.TripleCell.score, OAI.Problem358.PositiveFacet.surfaceFace

theorem OAI.Problem358.PositiveFacet.strictTieGraph_connected_of_positive_cells line 522
Source documentation
No generic-position, no facet positivity, and no strict-activation premise is left in this connectivity statement: all are consequences of positive cell masses and absolute continuity of the source.
```
theorem strictTieGraph_connected_of_positive_cells [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0) :
    (strictTieGraph K (fun i => TripleCell.score (y i) (c i))).Connected := by
…
```
Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.PositiveFacet.strictTieGraph, OAI.Problem358.TripleCell.score

theorem OAI.Problem358.PositiveFacet.exists_connected_surface_graph_of_positive_cells line 535

Source documentation

The exact positive-surface connectivity conclusion for positive-mass convex cells. Surface measures can be independently selected on each tangent hyperplane; fixed affine-plane basepoints are explicitly permitted.

theorem exists_connected_surface_graph_of_positive_cells [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0) :
    ∃ G : SimpleGraph ι, G.Connected ∧ ∀ i j, G.Adj i j →
      ∀ base : E d,
      (⟪base, y i⟫_ℝ + c i = ⟪base, y j⟫_ℝ + c j) →
      ∀ μ : Measure ((ℝ ∙ (y i - y j))ᗮ), IsOpenPosMeasure μ →
        0 < μ ((fun w : (ℝ ∙ (y i - y j))ᗮ => base + (w : E d)) ⁻¹'
          (CellGeometry.closedCell K y c i ∩ CellGeometry.closedCell K y c j)) := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.PositiveFacet.exists_connected_normalized_surface_graph line 554

Source documentation

The weighted graph needed by the cell-Laplacian range theorem, with normalized geometric face coefficients rather than assumed positive weights.

theorem exists_connected_normalized_surface_graph [Nonempty ι]
    (ρ : Measure (E d)) (hρ : ρ ≪ volume)
    (K : Set (E d)) (hK : IsCompact K) (hconv : Convex ℝ K)
    (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
    (hpos : ∀ i, ρ (CellGeometry.closedCell K y c i) ≠ 0) :
    ∃ G : SimpleGraph ι, G.Connected ∧ ∀ i j, G.Adj i j →
      ∀ base : E d,
      (⟪base, y i⟫_ℝ + c i = ⟪base, y j⟫_ℝ + c j) →
      ∀ μ : Measure ((ℝ ∙ (y i - y j))ᗮ),
        IsOpenPosMeasure μ → IsFiniteMeasureOnCompacts μ →
        0 < (μ (surfaceFace K y c i j base)).toReal /
          ((volume K).toReal * ‖y i - y j‖) := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.PositiveFacet.surfaceFace