Coarse-graining support: Support.Sobolev.Fractional.ContinuousInterpolation.TriadicScale

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

Triadic scale calculus for the continuous K-functional

This module contains only the convention-neutral conversion between the continuous scale variable in the exact K-seminorm and its canonical triadic samples. The intervals use (t_{j+1}, t_j] ∩ (0,1): this makes them disjoint and removes the endpoint at which the open-scale representative is totalized to zero.

noncomputable def HCPolySupport.triadicContinuousKScale (j : ℕ) : ↑ContinuousKScale

The canonical triadic member of the source scale carrier: t_j = 3^{-j}.

Equations

• HCPolySupport.triadicContinuousKScale j = ⟨3⁻¹ ^ j, ⋯⟩

@[simp]

theorem HCPolySupport.triadicContinuousKScale_zero : triadicContinuousKScale 0 = ⟨1, triadicContinuousKScale_zero._proof_1⟩

theorem HCPolySupport.triadicContinuousKScale_pos (j : ℕ) : 0 < ↑(triadicContinuousKScale j)

theorem HCPolySupport.triadicContinuousKScale_le_one (j : ℕ) : ↑(triadicContinuousKScale j) ≤ 1

theorem HCPolySupport.triadicContinuousKScale_succ (j : ℕ) : ↑(triadicContinuousKScale (j + 1)) = ↑(triadicContinuousKScale j) / 3

theorem HCPolySupport.triadicContinuousKScale_succ_lt (j : ℕ) : ↑(triadicContinuousKScale (j + 1)) < ↑(triadicContinuousKScale j)

theorem HCPolySupport.triadicContinuousKScale_antitone {j k : ℕ} (hjk : j ≤ k) : ↑(triadicContinuousKScale k) ≤ ↑(triadicContinuousKScale j)

def HCPolySupport.triadicContinuousKInterval (j : ℕ) : Set ℝ

The disjoint scale interval associated to the sample at depth j.

Equations

• HCPolySupport.triadicContinuousKInterval j = Set.Ioc ↑(HCPolySupport.triadicContinuousKScale (j + 1)) ↑(HCPolySupport.triadicContinuousKScale j) ∩ Set.Ioo 0 1

theorem HCPolySupport.measurableSet_triadicContinuousKInterval (j : ℕ) : MeasurableSet (triadicContinuousKInterval j)

theorem HCPolySupport.triadicContinuousKInterval_subset_openScale (j : ℕ) : triadicContinuousKInterval j ⊆ Set.Ioo 0 1

theorem HCPolySupport.mem_triadicContinuousKInterval_iff (j : ℕ) {t : ℝ} : t ∈ triadicContinuousKInterval j ↔ ↑(triadicContinuousKScale (j + 1)) < t ∧ t ≤ ↑(triadicContinuousKScale j) ∧ 0 < t ∧ t < 1

theorem HCPolySupport.triadicContinuousKInterval_pairwiseDisjoint : Pairwise fun (j k : ℕ) => Disjoint (triadicContinuousKInterval j) (triadicContinuousKInterval k)

theorem HCPolySupport.iUnion_triadicContinuousKInterval : ⋃ (j : ℕ), triadicContinuousKInterval j = Set.Ioo 0 1

The triadic intervals form a disjoint partition of the exact open scale interval. The choice (t_{j+1},t_j] assigns every triadic endpoint to its finer neighbor, while the extra intersection removes 1.

theorem HCPolySupport.continuousKFunctional_bounds_on_triadicContinuousKInterval {d : ℕ} (F : UnitCubeEuclideanL2Field d) (j : ℕ) {t : ℝ} (ht : t ∈ triadicContinuousKInterval j) : continuousKFunctional (triadicContinuousKScale (j + 1)) F ≤ continuousKFunctional ⟨t, ⋯⟩ F ∧ continuousKFunctional ⟨t, ⋯⟩ F ≤ continuousKFunctional (triadicContinuousKScale j) F

On a triadic interval, the sampled K-functional at the lower endpoint is bounded by the continuous value, which is bounded by the upper sample.

noncomputable def HCPolySupport.triadicContinuousKLowerSampleWeight {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (j : ℕ) : ENNReal

The lower sampled square-weight used for a single triadic interval.

Equations

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

noncomputable def HCPolySupport.triadicContinuousKUpperSampleWeight {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (j : ℕ) : ENNReal

The upper sampled square-weight used for a single triadic interval.

Equations

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

theorem HCPolySupport.triadicContinuousKInterval_lintegral_bounds {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (j : ℕ) : triadicContinuousKLowerSampleWeight s F j * MeasureTheory.volume (triadicContinuousKInterval j) ≤ ∫⁻ (t : ℝ) in triadicContinuousKInterval j, continuousKSeminormIntegrand (↑s) F t ∧ ∫⁻ (t : ℝ) in triadicContinuousKInterval j, continuousKSeminormIntegrand (↑s) F t ≤ triadicContinuousKUpperSampleWeight s F j * MeasureTheory.volume (triadicContinuousKInterval j)

A two-sided comparison of one continuous weighted scale interval with its two adjacent sampled weighted squares. It is valid in ℝ≥0∞ with no finiteness assumption.