OnePointChainPath

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Reading the cube geometry inside a larger carrier

The hit-then-exit chaining estimate is stated for a process of the state space in which the cubes live. The process produced by the divergence-form chain is a process of a larger carrier, the state space being read inside it by an open embedding. This file supplies the two deterministic ingredients needed to move the chaining input across that reading.

The first is a corestriction: a continuous path of the larger carrier all of whose values are images is the image of a continuous path of the state space. Only the fact that the reading is a topological embedding is used, through Topology.IsEmbedding.continuous_iff.

The second is the geometry of the padded cube families read inside the carrier. The padded closed cells are compact, so their images are compact and their union is closed; the padded enlargements are open, so their images are open; and the overlap count is unchanged because the reading is injective.

Main results

• exists_pathPostcomp_eq_of_forall_mem_range — the corestriction of a path with image values.
• exists_pathPostcomp_eq_of_exitTime_range_eq_top — the same from an infinite exit time from the image of the state space.
• isClosed_iUnion_image_enumeratedClosedCubeFamily, isOpen_image_enumeratedOpenEnlargementFamily, image_enumeratedCubeFamily_overlap — the hypotheses of the chaining estimate for the read families.

1. Corestriction of a continuous path along an embedding

theorem Algsuperdiff.Section5.Provider.exists_pathPostcomp_eq_of_forall_mem_range {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (e : C(alpha, beta)) (he : Topology.IsEmbedding ⇑e) (omega : MarkovProcess.ContinuousPath beta) (hmem : ∀ (t : NNReal), omega t ∈ Set.range ⇑e) : ∃ (w : MarkovProcess.ContinuousPath alpha), DivergenceFormProcess.LiveRestriction.pathPostcomp e w = omega

A path with image values is an image path. If every value of a continuous path of beta lies in the range of a topological embedding e, the path is the post-composition of a continuous path of alpha with e. Continuity of the corestriction is exactly the embedding criterion.

theorem Algsuperdiff.Section5.Provider.exists_pathPostcomp_eq_of_exitTime_range_eq_top {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [PseudoMetricSpace beta] (e : C(alpha, beta)) (he : Topology.IsEmbedding ⇑e) (omega : MarkovProcess.ContinuousPath beta) (htop : MarkovProcess.ContinuousPath.exitTime (Set.range ⇑e) omega = ⊤) : ∃ (w : MarkovProcess.ContinuousPath alpha), DivergenceFormProcess.LiveRestriction.pathPostcomp e w = omega

A path that never leaves the image is an image path. An infinite exit time from the range of the reading map says exactly that every value of the path is an image.

2. The padded cube families read inside a carrier

theorem Algsuperdiff.Section5.Provider.isCompact_enumeratedClosedCubeFamily {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : IsCompact (Trace.enumeratedClosedCubeFamily n sites i)

The padded closed cells are compact: each is a closed ball of the state space or empty.

theorem Algsuperdiff.Section5.Provider.isCompact_iUnion_enumeratedClosedCubeFamily {d r : ℕ} (n : ℤ) (sites : Fin r ↪ Percolation.Site d) : IsCompact (⋃ (i : ℕ), Trace.enumeratedClosedCubeFamily n sites i)

The union of the padded closed cells is compact: only finitely many members are nonempty.

theorem Algsuperdiff.Section5.Provider.measurableSet_image_enumeratedClosedCubeFamily {d r : ℕ} {alpha : Type u_1} [MetricSpace alpha] (emb : C(HCPolySupport.Vec d, alpha)) [MeasurableSpace alpha] [BorelSpace alpha] (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : MeasurableSet (⇑emb '' Trace.enumeratedClosedCubeFamily n sites i)

Every read padded cell is measurable, being the continuous image of a compact set.

theorem Algsuperdiff.Section5.Provider.isClosed_iUnion_image_enumeratedClosedCubeFamily {d r : ℕ} {alpha : Type u_1} [MetricSpace alpha] (emb : C(HCPolySupport.Vec d, alpha)) (n : ℤ) (sites : Fin r ↪ Percolation.Site d) : IsClosed (⋃ (i : ℕ), ⇑emb '' Trace.enumeratedClosedCubeFamily n sites i)

The union of the read padded cells is closed, being the continuous image of a compact set.

theorem Algsuperdiff.Section5.Provider.isOpen_image_enumeratedOpenEnlargementFamily {d r : ℕ} {alpha : Type u_1} [MetricSpace alpha] (emb : C(HCPolySupport.Vec d, alpha)) (hemb : Topology.IsOpenEmbedding ⇑emb) (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : IsOpen (⇑emb '' Trace.enumeratedOpenEnlargementFamily n sites i)

Every read padded enlargement is open, the reading being an open map.

theorem Algsuperdiff.Section5.Provider.image_enumeratedCubeFamily_overlap {d r : ℕ} {alpha : Type u_1} [MetricSpace alpha] (emb : C(HCPolySupport.Vec d, alpha)) (hemb : Function.Injective ⇑emb) (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (i : ℕ) : ∃ (s : Finset ℕ), s.card ≤ 3 ^ d ∧ ∀ (j : ℕ), (⇑emb '' Trace.enumeratedClosedCubeFamily n sites j ∩ ⇑emb '' Trace.enumeratedOpenEnlargementFamily n sites i).Nonempty → j ∈ s

The overlap count of the read families is the overlap count of the families themselves: an injective reading neither creates nor destroys an intersection.