Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.TriadicScale

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_mem_Icc (n : ℕ) : 1 / 3 ≤ coarseCaccioppoliRadiusSequence n ∧ coarseCaccioppoliRadiusSequence n ≤ 1

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_lt_one (n : ℕ) : coarseCaccioppoliRadiusSequence n < 1

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_strictMono : StrictMono coarseCaccioppoliRadiusSequence

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_succ_sub (n : ℕ) : coarseCaccioppoliRadiusSequence (n + 1) - coarseCaccioppoliRadiusSequence n = 2 / (3 * ↑((n + 1) * (n + 2)))

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_gap_pos (n : ℕ) : 0 < coarseCaccioppoliRadiusSequence (n + 1) - coarseCaccioppoliRadiusSequence n

theorem HCPolySupport.coarseCaccioppoliRadiusIterationTerm_nonneg (β : ℝ) (n : ℕ) : 0 ≤ coarseCaccioppoliRadiusIterationTerm β n

theorem HCPolySupport.coarseCaccioppoliGapInv_nonneg {ρ₁ ρ₂ : ℝ} (hρ : ρ₁ < ρ₂) : 0 ≤ coarseCaccioppoliGapInv ρ₁ ρ₂

@[simp]

theorem HCPolySupport.coarseCaccioppoliGapInv_eq_inv (ρ₁ ρ₂ : ℝ) : coarseCaccioppoliGapInv ρ₁ ρ₂ = (ρ₂ - ρ₁)⁻¹

theorem HCPolySupport.coarseCaccioppoli_gap_le_two_thirds {ρ₁ ρ₂ : ℝ} (hρ₁ : 1 / 3 ≤ ρ₁) (_hlt : ρ₁ < ρ₂) (hρ₂ : ρ₂ ≤ 1) : ρ₂ - ρ₁ ≤ 2 / 3

theorem HCPolySupport.exists_coarseCaccioppoliTriadicGapScaleChoice {ρ₁ ρ₂ : ℝ} (hρ₁ : 1 / 3 ≤ ρ₁) (hlt : ρ₁ < ρ₂) (hρ₂ : ρ₂ ≤ 1) : ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂

There is always a triadic scale in the note's admissible gap window.

noncomputable def HCPolySupport.coarseCaccioppoliTriadicGapScale (ρ₁ ρ₂ : ℝ) : ℕ

A canonical triadic scale choice for the radius gap. Outside the Caccioppoli radius range it is set to 0; all note-facing uses go through the _spec lemma below.

Equations

• HCPolySupport.coarseCaccioppoliTriadicGapScale ρ₁ ρ₂ = if h : 1 / 3 ≤ ρ₁ ∧ ρ₁ < ρ₂ ∧ ρ₂ ≤ 1 then Classical.choose ⋯ else 0

theorem HCPolySupport.coarseCaccioppoliTriadicGapScale_spec {ρ₁ ρ₂ : ℝ} (hρ₁ : 1 / 3 ≤ ρ₁) (hlt : ρ₁ < ρ₂) (hρ₂ : ρ₂ ≤ 1) : CoarseCaccioppoliTriadicGapScaleChoice (coarseCaccioppoliTriadicGapScale ρ₁ ρ₂) ρ₁ ρ₂

theorem HCPolySupport.coarseCaccioppoliGapInv_ge_three_halves {ρ₁ ρ₂ : ℝ} (hρ₁ : 1 / 3 ≤ ρ₁) (hlt : ρ₁ < ρ₂) (hρ₂ : ρ₂ ≤ 1) : 3 / 2 ≤ coarseCaccioppoliGapInv ρ₁ ρ₂

theorem HCPolySupport.coarseCaccioppoli_pow_scale_le_mul_gapInv_of_triadicGapScaleChoice {k : ℕ} {ρ₁ ρ₂ : ℝ} (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hρ : ρ₁ < ρ₂) : 3 ^ k ≤ 81 * coarseCaccioppoliGapInv ρ₁ ρ₂

theorem HCPolySupport.coarseCaccioppoli_mul_gapInv_le_pow_scale_of_triadicGapScaleChoice {k : ℕ} {ρ₁ ρ₂ : ℝ} (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hρ : ρ₁ < ρ₂) : 27 * coarseCaccioppoliGapInv ρ₁ ρ₂ ≤ 3 ^ k

theorem HCPolySupport.coarseCaccioppoli_boundary_noteAbsorptionCondition_of_triadicGapScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C / (s * (1 - s)) * 3 ^ k * Real.rpow 3 (-coarseCaccioppoliSigma s t * h ρ₁ ρ₂) * (ThetaRatio Q s t a).rpow (1 / 2) ≤ 27 / 4) : CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h

A stronger triadic-scale absorption estimate, stated using the note's auxiliary scale k, implies the actual absorption condition appearing in the boundary coefficient bookkeeping.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteAbsorptionCondition_of_heightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hheight : CoarseCaccioppoliBoundaryHeightChoice Q a s t C h) : CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h

The note-facing explicit height choice already implies the absorbability condition in the boundary bookkeeping.

theorem HCPolySupport.coarseCaccioppoli_interior_noteAbsorptionCondition_of_triadicGapScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C / (s * (1 - s)) * 3 ^ k * Real.rpow 3 (-coarseCaccioppoliSigma s t * h ρ₁ ρ₂) * (ThetaRatio Q s t a).rpow (1 / 2) ≤ 27 / 4) : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h

The interior note-specific absorption condition currently follows from the same stronger triadic-scale estimate as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_interior_noteAbsorptionCondition_of_heightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hheight : CoarseCaccioppoliInteriorHeightChoice Q a s t C h) : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h

The same explicit h-choice bookkeeping also discharges the interior absorption condition.