Weak tiling problems
Problem 4.3.* Let be a finite union of intervals and a weak tiling measure for . Must be expressible as a convex combination of proper tiling measures?
Mathematical statement
Problem 4.3.* Let be a finite union of intervals and a weak tiling measure for . Must be expressible as a convex combination of proper tiling measures?
Statement source: Papers statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
problem_4_3
theorem problem_4_3 : answer(sorry) ↔ ∀ (Ω : Set ℝ) (_ : IsFiniteUnionOfIntervals Ω) (ν : Measure ℝ) (_ : IsWeakTilingMeasure Ω ν), ∃ (T : ℕ → Set ℝ) (c : ℕ → ℝ≥0), (∀ i, IsProperTiling Ω (T i)) ∧ ∑' i : ℕ, c i = 1 ∧ ν = Measure.sum (fun i => (c i : ℝ≥0∞) • Measure.sum (fun t : T i => Measure.dirac (t : ℝ))) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References