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

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

theorem HCPolySupport.coarseCaccioppoli_sigma_pos {s t : ℝ} (hst : s + t < 1) : 0 < coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_beta_nonneg {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliBeta s t

theorem HCPolySupport.coarseCaccioppoli_power_nonneg {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliPower s t

theorem HCPolySupport.coarseCaccioppoli_sigma_le_one_sub_s {s t : ℝ} (ht : 0 < t) : coarseCaccioppoliSigma s t ≤ 1 - s

theorem HCPolySupport.coarseCaccioppoli_sigma_div_one_sub_s_le_one {s t : ℝ} (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliSigma s t / (1 - s) ≤ 1

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_beta {s t : ℝ} (hst : s + t < 1) : coarseCaccioppoliSigma s t * coarseCaccioppoliBeta s t = 2 * (1 - t)

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_power {s t : ℝ} (hst : s + t < 1) : coarseCaccioppoliSigma s t * coarseCaccioppoliPower s t = 2 * s

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_beta_le_two {s t : ℝ} (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliSigma s t * coarseCaccioppoliBeta s t ≤ 2

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_power_le_two {s t : ℝ} (_hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliSigma s t * coarseCaccioppoliPower s t ≤ 2

theorem HCPolySupport.coarseCaccioppoli_beta_eq_two_add_power {s t : ℝ} (hst : s + t < 1) : coarseCaccioppoliBeta s t = 2 + coarseCaccioppoliPower s t

theorem HCPolySupport.coarseCaccioppoli_beta_ge_two {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 2 ≤ coarseCaccioppoliBeta s t

theorem HCPolySupport.coarseCaccioppoli_natCeil_beta_le_two_mul_beta {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : ↑⌈coarseCaccioppoliBeta s t⌉₊ ≤ 2 * coarseCaccioppoliBeta s t

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_natCeil_beta_le_four {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliSigma s t * ↑⌈coarseCaccioppoliBeta s t⌉₊ ≤ 4

theorem HCPolySupport.coarseCaccioppoli_power_ge_two_mul_s {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 2 * s ≤ coarseCaccioppoliPower s t

theorem HCPolySupport.coarseCaccioppoli_beta_ge_two_add_two_mul_s {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 2 + 2 * s ≤ coarseCaccioppoliBeta s t

theorem HCPolySupport.coarseCaccioppoli_noteExponent_eq_two_mul_beta_sub_two {s t : ℝ} (hst : s + t < 1) : 2 + 4 * s / coarseCaccioppoliSigma s t = 2 * coarseCaccioppoliBeta s t - 2

theorem HCPolySupport.coarseCaccioppoli_noteExponent_pos {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 0 < 2 + 4 * s / coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_noteExponent_ge_one {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 1 ≤ 2 + 4 * s / coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_beta_le_noteExponent {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : coarseCaccioppoliBeta s t ≤ 2 + 4 * s / coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_power_le_noteExponent {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : coarseCaccioppoliPower s t ≤ 2 + 4 * s / coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_power_div_noteExponent_le_one {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : coarseCaccioppoliPower s t / (2 + 4 * s / coarseCaccioppoliSigma s t) ≤ 1

theorem HCPolySupport.coarseCaccioppoli_two_natCeil_beta_sub_four_le_noteExponent {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) : 2 * ↑⌈coarseCaccioppoliBeta s t⌉₊ - 4 ≤ 2 + 4 * s / coarseCaccioppoliSigma s t

The note exponent dominates the integerized radius exponent, up to the fixed four-unit loss from taking a ceiling.

theorem HCPolySupport.coarseCaccioppoli_natCeil_beta_le_noteExponent_of_four_le {s t : ℝ} (hs : 0 < s) (hst : s + t < 1) (hk : 4 ≤ ⌈coarseCaccioppoliBeta s t⌉₊) : ↑⌈coarseCaccioppoliBeta s t⌉₊ ≤ 2 + 4 * s / coarseCaccioppoliSigma s t

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_noteExponent_le_four {s t : ℝ} (_hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliSigma s t * (2 + 4 * s / coarseCaccioppoliSigma s t) ≤ 4

theorem HCPolySupport.rpow_neg_self_le_exp_one {r : ℝ} (hr : 0 < r) (_hr_le : r ≤ 1) : r.rpow (-r) ≤ Real.exp 1

Entropy-type scalar bound used in the Caccioppoli constant extraction. For 0 < r ≤ 1, the factor r^{-r} is uniformly bounded by exp 1. This is the one-variable cancellation behind the small-s branch of the note constant.

theorem HCPolySupport.rpow_neg_two_mul_self_le_exp_two {r : ℝ} (hr : 0 < r) (_hr_le : r ≤ 1) : r.rpow (-(2 * r)) ≤ Real.exp 2

A two-fold version of rpow_neg_self_le_exp_one.

theorem HCPolySupport.coarseCaccioppoli_sigma_mul_singularRoot_le_exp_two {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : have σ := coarseCaccioppoliSigma s t; have q := coarseCaccioppoliPower s t; have p := 2 + 4 * s / σ; σ * s.rpow (-(q / p)) * (1 - s).rpow (-(q / p)) ≤ Real.exp 2

The singular scalar factors left after taking the note-exponent root are uniformly bounded. This is the explicit s,t cancellation in the Caccioppoli constant extraction.

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale_ge_k_add_four {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ↑k + 4 ≤ coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C k

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale_le_localizedExplicitHeightAtScale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C k ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale_ge_k_add_four {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ↑k + 4 ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale_ge_four_div_s {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : 4 / s ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale_ge_four_div_s_add_t {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s t C : ℝ} (k : ℕ) (hs : 0 < s) (ht : 0 < t) : 4 / (s + t) ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ℕ

Natural depth obtained by integerizing the localized explicit height. This is the depth used by the small-cube Caccioppoli route.

Equations

• HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k = ⌈HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k⌉₊

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) : ℝ → ℝ → ℕ

Radius-indexed integerized localized height depth.

Equations

• HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice Q a s t C k ρ₁ ρ₂ = HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C (k ρ₁ ρ₂)

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryIntegerizedLocalizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) : ℝ → ℝ → ℝ

Real-valued height associated to the integerized localized depth.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale_le_depth {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k ≤ ↑(coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k)

The integerized localized depth dominates the localized real height.

theorem HCPolySupport.coarseCaccioppoliBoundaryIntegerizedLocalizedExplicitHeightAtScale_ge_k_add_four {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ↑k + 4 ≤ ↑(coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k)

The integerized localized height keeps the k + 4 lower bound.

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale_ge_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : k ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k

The integerized localized depth is at least the triadic gap scale.

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice_ge_scaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) (ρ₁ ρ₂ : ℝ) : k ρ₁ ρ₂ ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice Q a s t C k ρ₁ ρ₂

Radius-indexed version of coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale_ge_scale.

theorem HCPolySupport.coarseCaccioppoliBoundaryIntegerizedLocalizedExplicitHeightAtScale_ge_four_div_s {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : 4 / s ≤ ↑(coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k)

The integerized localized height keeps the 4 / s lower bound.

theorem HCPolySupport.coarseCaccioppoliBoundaryIntegerizedLocalizedExplicitHeightAtScale_ge_four_div_s_add_t {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s t C : ℝ} (k : ℕ) (hs : 0 < s) (ht : 0 < t) : 4 / (s + t) ≤ ↑(coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k)

The integerized localized height keeps the 4 / (s + t) lower bound.

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale_logBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) (hst : s + t < 1) : Real.log (coarseCaccioppoliBoundaryHeightLogArg Q a s t C k) ≤ coarseCaccioppoliSigma s t * coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C k * Real.log 3

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale_absorption {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : C / (s * (1 - s)) * 3 ^ k * Real.rpow 3 (-coarseCaccioppoliSigma s t * coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C k) * (ThetaRatio Q s t a).rpow (1 / 2) ≤ 1 / 4

theorem HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale_absorption {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : C / (s * (1 - s)) * 3 ^ k * Real.rpow 3 (-coarseCaccioppoliSigma s t * coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k) * (ThetaRatio Q s t a).rpow (1 / 2) ≤ 1 / 4

theorem HCPolySupport.coarseCaccioppoli_boundary_heightChoice_of_explicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) : CoarseCaccioppoliBoundaryHeightChoice Q a s t C (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)

theorem HCPolySupport.coarseCaccioppoli_interior_heightChoice_of_explicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) : CoarseCaccioppoliInteriorHeightChoice Q a s t C (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)

theorem HCPolySupport.coarseCaccioppoli_boundary_heightChoice_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) : CoarseCaccioppoliBoundaryHeightChoice Q a s t C (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k)

theorem HCPolySupport.coarseCaccioppoli_interior_heightChoice_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) : CoarseCaccioppoliInteriorHeightChoice Q a s t C (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k)

@[simp]

theorem HCPolySupport.coarseCaccioppoliRadiusSequence_zero : coarseCaccioppoliRadiusSequence 0 = 1 / 3