LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Characteristic departure cells are measurable and have positive finite volume

Statement

Assume the Axiom of Countable Choice. Let $Ω = \prod_{j = 1}^{d} (0, ℓ_{j})$ be the bounded open fundamental box used for Lebesgue measure, and let $Q = \prod_{j = 1}^{d} [0, ℓ_{j})$ be its half-open grid-indexing copy. Let $Φ$ be the periodic $C^{1}$ characteristic diffeomorphism of A periodic C1 characteristic map is an orientation-preserving diffeomorphism, and let $A_{i} \subseteq Q$ be a Lebesgue-measurable arrival cell with $∣ A_{i} ∣ : = λ_{d} (A_{i} \cap Ω) > 0$ . Then $D_{i} : = Φ^{- 1} (A_{i})$ , interpreted on the torus and represented in $Ω$ , is Lebesgue measurable and satisfies $0 < ∣ D_{i} ∣ < \infty .$ This includes every finite tensor-grid cell with nonempty interior. The departure cells form a partition up to null sets whenever a finite family of arrival cells does; an exact torus partition pulls back to an exact torus partition.

Facts & Assumptions

Given: Countable Choice, a periodic $C^{1}$ characteristic diffeomorphism, the fundamental boxes $Ω, Q$ , and measurable positive-volume arrival cells.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is assumed for the Lebesgue-measure suppliers below; no additional choice is used.

[F1]

A periodic C1 characteristic map is an orientation-preserving diffeomorphism gives the lifted flow and its inverse as $C^{1}$ diffeomorphisms; A periodic C1 velocity has a global characteristic flow on a finite horizon gives their equivariance under the period lattice.

[F2]

A C^1 diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets: under Countable Choice a $C^{1}$ diffeomorphism between open Euclidean sets maps measurable sets to measurable sets. Apply this also to translations and to $Φ^{- 1}$ .

[F3]

A C^1 diffeomorphism maps Lebesgue null sets to Lebesgue null sets: under Countable Choice the same maps preserve null sets.

[F4]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume and Finite and countable subadditivity of measures: measurable sets form a sigma-algebra, Lebesgue measure is complete, and a countable union of null sets is null.

[F5]

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included: $∣ Ω ∣ = \prod_{j} ℓ_{j} < \infty$ ; bounded boxes with a degenerate side are null. Thus the union $H : = ⋃_{j = 1}^{d} ⋃_{k \in Z} {x : x_{j} = k ℓ_{j}}$ of tile faces is null, by covering each face with countably many bounded degenerate boxes and applying [F4].

[F6]

Measures are monotone: measurable inclusions preserve measure order.

Proof

1.1givenA1F1F2F4construct

Put $Λ = \prod_{j} ℓ_{j} Z$ and ${\hat{A}}_{i} = ⋃_{k \in Λ} (A_{i} + k)$ . By [F2] and [F4] this countable periodic lift is measurable, and $E_{i} : = Φ^{- 1} ({\hat{A}}_{i})$ is measurable by [F1] and [F2]. Hence $D_{i} = E_{i} \cap Ω$ is measurable. Equivariance makes $E_{i}$ periodic and makes the torus preimage independent of representatives.

2.1givenA1F1F3F4F5F6step 1.1algebra

If $∣ D_{i} ∣ = 0$ , [F3] and [F4] make $⋃_{k \in Λ} (D_{i} + k)$ null. Every point of $E_{i}$ outside $H$ lies in one open tile, so periodicity gives $E_{i} \subseteq H \cup ⋃_{k \in Λ} (D_{i} + k)$ . By [F4] and [F5], $E_{i}$ is null; [F3] then makes $Φ (E_{i}) = {\hat{A}}_{i}$ null. This contradicts $A_{i} \cap Ω \subseteq {\hat{A}}_{i}$ and $∣ A_{i} ∣ > 0$ by [F6]. Thus $∣ D_{i} ∣ > 0$ . Also $D_{i} \subseteq Ω$ , so [F5] and [F6] give $∣ D_{i} ∣ \leq \prod_{j} ℓ_{j} < \infty$ .

3.1givenA1F1F3F4F5F6step 1.1step 2.1algebra∎

Bijectivity on the torus preserves exact unions and disjointness. For a partition only up to null sets, lift its omitted set and pairwise overlaps periodically; these are null by [F3]–[F5]. Their inverse images are null by [F1] and [F3], so restricting to $Ω$ gives a departure partition up to null sets. Finally, a half-open tensor cell with nonempty interior is measurable with positive volume by [F5], so it is included in the result.

Depends on

Used by

Dependency tree · two levels

52 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

European Centre for Medium-Range Weather Forecasts, Numerical Methods, Meteorological Training Course Lecture Series, 2002 (standard reference, not scraped)
Lukas Einkemmer and Alexander Ostermann, On the error propagation of semi-Lagrange and Fourier methods for advection problems, Computers & Mathematics with Applications 69 (2015), 170–179 (standard reference, not scraped)