Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ProbeMax

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

Normalized finite-probe maxima

The quenched minimal-scale theorem needs one random observable which controls the localized response for every unit vector. The finite-basis reduction allows this observable to be a finite maximum over normalized coordinate and pair probes.

inductive HCPolySupport.Book.Ch05.Section57.NormalizedProbeKind : Type

The three finite probe types: coordinate, sum of two coordinates, and difference of two coordinates.

• coord : NormalizedProbeKind
• plus : NormalizedProbeKind
• minus : NormalizedProbeKind

@[instance_reducible]

instance HCPolySupport.Book.Ch05.Section57.instDecidableEqNormalizedProbeKind : DecidableEq NormalizedProbeKind

Equations

• HCPolySupport.Book.Ch05.Section57.instDecidableEqNormalizedProbeKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HCPolySupport.Book.Ch05.Section57.instFintypeNormalizedProbeKind : Fintype NormalizedProbeKind

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section57.fintype_card_normalizedProbeKind : Fintype.card NormalizedProbeKind = 3

@[reducible, inline]

abbrev HCPolySupport.Book.Ch05.Section57.NormalizedProbeIndex (d : ℕ) : Type

The finite probe index set used to eliminate the continuum of unit vectors.

Equations

• HCPolySupport.Book.Ch05.Section57.NormalizedProbeIndex d = (HCPolySupport.BlockCoord d × HCPolySupport.BlockCoord d × HCPolySupport.Book.Ch05.Section57.NormalizedProbeKind)

noncomputable def HCPolySupport.Book.Ch05.Section57.normalizedProbeVec {d : ℕ} : NormalizedProbeIndex d → FullBlockVec d

Coordinate probes are already normalized; plus/minus probes are divided by two.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.normalizedProbeVec_dotProduct_self_le_one {d : ℕ} (i : NormalizedProbeIndex d) : normalizedProbeVec i ⬝ᵥ normalizedProbeVec i ≤ 1

theorem HCPolySupport.Book.Ch05.Section57.normalizedProbeVec_abs_apply_le_one {d : ℕ} (i : NormalizedProbeIndex d) (α : BlockCoord d) : |normalizedProbeVec i α| ≤ 1

noncomputable def HCPolySupport.Book.Ch05.Section57.localizedNormalizedProbeJMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m n : ℕ) : RegCoeffField d → ℝ

Localized maximum over the normalized finite probe family.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJNormalizedProbeSumMax_le_probeJMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} (hnm : n ≤ m) (a : RegCoeffField d) : localizedLimitNormalizedJNormalizedProbeSumMax hP hStruct m n a ≤ ↑(Fintype.card (NormalizedProbeIndex d)) * localizedNormalizedProbeJMax hP hStruct m n a

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_le_normalizedProbeJMax_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) : localizedLimitNormalizedJMax hP hStruct m n e ≤ᵐ[P] fun (a : RegCoeffField d) => 4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d)) * localizedNormalizedProbeJMax hP hStruct m n a

theorem HCPolySupport.Book.Ch05.Section57.localizedNormalizedProbeJMax_sub_const_le_sup_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} (c : ℝ) (a : RegCoeffField d) : have S := Finset.univ; ∀ (hS : S.Nonempty), localizedNormalizedProbeJMax hP hStruct m n a - c ≤ S.sup' hS fun (i : NormalizedProbeIndex d) => localizedLimitNormalizedJMax hP hStruct m n (normalizedProbeVec i) a - c

theorem HCPolySupport.Book.Ch05.Section57.localizedFirstQuenchedEstimate_normalizedProbeJMax {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (α : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < α ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {ℓ n m : ℕ}, ℓ < n → n < m → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; IndependentSums.IsBigOWith P (IndependentSums.gammaSigma (min σ 2)) (fun (a : RegCoeffField d) => localizedNormalizedProbeJMax hP hStruct (N0 + m) (N0 + n) a - Real.rpow 3 (-α * ↑ℓ)) ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2)))

Localized first-quenched estimate for the normalized finite-probe maximum.

This is the fixed-vector localized estimate, applied to the finite normalized probe family and combined by the Chapter 4 finite-maximum rule.

theorem HCPolySupport.Book.Ch05.Section57.localizedFirstQuenchedEstimate_normalizedProbeJMax_uniformAnnealedExponent {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {ℓ n m : ℕ}, ℓ < n → n < m → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; IndependentSums.IsBigOWith P (IndependentSums.gammaSigma (min σ 2)) (fun (aω : RegCoeffField d) => localizedNormalizedProbeJMax hP hStruct (N0 + m) (N0 + n) aω - Real.rpow 3 (-a * ↑ℓ)) ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2)))

Uniform-in-σ version of localizedFirstQuenchedEstimate_normalizedProbeJMax.

theorem HCPolySupport.Book.Ch05.Section57.isBigO_localizedNormalizedProbeJMax {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {m n : ℕ}, n < m → have D := descendantsAtScale (originCube d ↑m) ↑n; have S := Finset.univ; IndependentSums.IsBigO P (IndependentSums.gammaSigma σ) (localizedNormalizedProbeJMax hP hStruct m n) ((3 * Real.log ↑S.card) ^ σ⁻¹ * ((3 * Real.log ↑D.card) ^ σ⁻¹ * (C * hΓ.thetaHat ^ 2)))

Crude Γσ estimate for the localized normalized finite-probe maximum.