ML.Core · Causalean Library

Hypothesis 3 core · 0 supporting The standalone ML spine carries two views of a learning method, connected later by Causalean.ML.Core.Bridge: * the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → ★ Predictor★ HypothesisClass★ FeatureMap

Hypothesis classes and parametrized predictors

The standalone ML spine carries two views of a learning method, connected later by Causalean.ML.Core.Bridge:

* the parametric view (Predictor): a parameter type Θ together with an admissible set and a prediction map Θ → X → Y. Optimization, convexity and regularization live here. * the extensional view (HypothesisClass): a set of measurable functions X → Y. Population-risk targets and best-in-class statements live here.

FeatureMap packages a feature transform X → (K → ℝ) so that linear-in-features regression (and hence series/sieve regression) is a single object.

structure Predictor reviewed

Causalean.ML

A parametrized family of predictors bundles an admissible set of parameter values together with a map sending each parameter to a prediction function from the covariates to the outcome.

Definition (Lean source)

parameters

Θ X Y :

Type*

fields

The admissible parameter set (e.g. a norm ball, or all of `Θ`).

paramSet :

Set Θ

The prediction map: a parameter yields a function `X → Y`.

predict :

Θ → X → Y

Causalean.ML.Predictor · Causalean/ML/Core/Hypothesis.lean:27

structure HypothesisClass reviewed

Causalean.ML

A hypothesis class packaged extensionally as a set of admissible prediction functions from the covariates to the outcome, subject to the requirement that every function admitted to the class is measurable.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

fields

The set of admissible prediction functions.

carrier :

Set (X → Y)

Every admissible function is measurable.

measurable :

∀ ⦃h : X → Y⦄

if

h ∈ carrier

then

Measurable h

Causalean.ML.HypothesisClass · Causalean/ML/Core/Hypothesis.lean:36

structure FeatureMap reviewed

Causalean.ML

A finite feature map bundles a transform sending each input to its vector of K feature values. Linear-in-features predictors use x ↦ ⟪β, φ x⟫; the identity feature map recovers ordinary linear regression, and other choices of the transform recover polynomial, spline, or Fourier (sieve) regression.

Definition (Lean source)

parameters

X :

Type*

K :

Type*

Fintype K

fields

The feature transform sending an input to its vector of feature values.

φ :

X → (K → ℝ)

Causalean.ML.FeatureMap · Causalean/ML/Core/Hypothesis.lean:45

Risk 7 core · 0 supporting Risk criteria for the ML spine, in both the parametric and extensional views. ★ Loss★ empiricalRisk★ populationRisk

Empirical and population risk

Risk criteria for the ML spine, in both the parametric and extensional views. Loss is a pointwise prediction-label loss, empiricalRisk and empiricalRiskP are nonempty finite-sample averages, populationRisk and populationRiskP are Bochner-integral population criteria, and iidEmpiricalRisk expresses empirical risk through Stat.IIDSample.sampleMean. The separate predicate HasFinitePopulationRisk records when the population integral has the usual finite expected-loss interpretation.

abbrev Loss reviewed

Causalean.ML

A pointwise loss: loss ŷ y compares a prediction ŷ to a label y.

Definition (Lean source)

abbrev Loss (Y : Type*) := Y → Y → ℝ

Causalean.ML.Loss · Causalean/ML/Core/Risk.lean:25

def empiricalRisk reviewed

Causalean.ML

The empirical risk criterion of a prediction rule is the sample loss sum scaled by the inverse cardinality of a nonempty finite sample index. The nonemptiness assumption rules out the empty-sample convention where the average would collapse to zero without data.

Definition (Lean source)

noncomputable def empiricalRisk {ι X Y : Type*} [Fintype ι] [Nonempty ι] (loss : Loss Y) (S : ι → X × Y) (h : X → Y) : ℝ := (Fintype.card ι : ℝ)⁻¹ * ∑ i, loss (h (S i).1) (S i).2

Causalean.ML.empiricalRisk · Causalean/ML/Core/Risk.lean:28 · uses Loss

def empiricalRiskP reviewed

Causalean.ML

The empirical risk criterion of a model parameter is the finite-sample criterion over a nonempty sample applied to the prediction rule selected by that parameter.

Definition (Lean source)

noncomputable def empiricalRiskP {ι Θ X Y : Type*} [Fintype ι] [Nonempty ι] (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (θ : Θ) : ℝ := empiricalRisk loss S (M.predict θ)

Causalean.ML.empiricalRiskP · Causalean/ML/Core/Risk.lean:36 · uses Loss , Predictor

def populationRisk reviewed

Causalean.ML

The population risk criterion of a prediction rule is the Bochner integral of its pointwise loss under the joint law. This definition does not by itself assert integrability or finite expected loss.

Definition (Lean source)

noncomputable def populationRisk {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (loss : Loss Y) (P : Measure (X × Y)) (h : X → Y) : ℝ := ∫ z, loss (h z.1) z.2 ∂P

Causalean.ML.populationRisk · Causalean/ML/Core/Risk.lean:43 · uses Loss

def populationRiskP reviewed

Causalean.ML

The population risk criterion of a model parameter is the Bochner-integral criterion applied to the prediction rule selected by that parameter.

Definition (Lean source)

noncomputable def populationRiskP {Θ X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (P : Measure (X × Y)) (θ : Θ) : ℝ := populationRisk loss P (M.predict θ)

Causalean.ML.populationRiskP · Causalean/ML/Core/Risk.lean:50 · uses Loss , Predictor

def iidEmpiricalRisk reviewed

Causalean.ML

The empirical risk along the first n points of an i.i.d. sample, expressed through Stat.IIDSample.sampleMean.

Definition (Lean source)

noncomputable def iidEmpiricalRisk {Ω X Y : Type*} [MeasurableSpace Ω] [MeasurableSpace (X × Y)] {μ : Measure Ω} {P : Measure (X × Y)} (S : IIDSample Ω (X × Y) μ P) (loss : Loss Y) (h : X → Y) (n : ℕ) : Ω → ℝ := S.sampleMean (fun z => loss (h z.1) z.2) n

Causalean.ML.iidEmpiricalRisk · Causalean/ML/Core/Risk.lean:56 · uses Loss , IIDSample

def HasFinitePopulationRisk reviewed

Causalean.ML

The loss-integrand of h is integrable, so the population risk is finite.

Definition (Lean source)

def HasFinitePopulationRisk {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (loss : Loss Y) (P : Measure (X × Y)) (h : X → Y) : Prop := Integrable (fun z => loss (h z.1) z.2) P

Causalean.ML.HasFinitePopulationRisk · Causalean/ML/Core/Risk.lean:65 · uses Loss

ERM 5 core · 0 supporting Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching t ★ IsERMP★ IsApproxERMP★ RegularizedERM★ IsERM★ IsPopulationRiskMinimizer

Empirical-risk-minimizer predicates

Minimizer predicates for the ML spine, stated candidate-wise via Mathlib's IsMinOn (or a comparison + ε form), never via sInf/argmin — this avoids pathological real-infimum defaults on empty or unbounded sets, matching the existing Estimation.OrthogonalLearning.PluginERM idiom.

The file provides exact, approximate, and regularized parametric ERM predicates (IsERMP, IsApproxERMP, RegularizedERM), plus extensional empirical and population minimizer predicates (IsERM, IsPopulationRiskMinimizer) over a HypothesisClass. The parametric and extensional views are connected in Causalean.ML.Core.Bridge.

structure IsERMP reviewed

Causalean.ML

θhat exactly minimizes a parametric objective over the admissible set.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

fields

The minimizer is admissible.

mem :

θhat ∈ Θset

It attains the minimum of the objective over `Θset`.

isMin :

IsMinOn objective Θset θhat

Causalean.ML.IsERMP · Causalean/ML/Core/ERM.lean:27

structure IsApproxERMP reviewed

Causalean.ML

θhat minimizes a parametric objective up to slack ε ≥ 0.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

Θset :

Set Θ

θhat :

Θ

ε :

ℝ

fields

The slack is nonnegative.

ε_nonneg :

0 ≤ ε

The candidate is admissible.

mem :

θhat ∈ Θset

Its objective is within `ε` of every competitor's.

approx_min :

∀ θ ∈ Θset, objective θhat ≤ objective θ + ε

Causalean.ML.IsApproxERMP · Causalean/ML/Core/ERM.lean:34

structure RegularizedERM reviewed

Causalean.ML

θhat minimizes a penalized objective objective θ + lam · penalty θ with a nonnegative regularization weight lam.

Definition (Lean source)

parameters

Θ :

Type*

objective :

Θ → ℝ

penalty :

Θ → ℝ

lam :

ℝ

Θset :

Set Θ

θhat :

Θ

fields

The regularization weight is nonnegative.

lam_nonneg :

0 ≤ lam

The minimizer is admissible.

mem :

θhat ∈ Θset

It minimizes the penalized objective over `Θset`.

isMin :

IsMinOn (fun θ => objective θ + lam * penalty θ) Θset θhat

Causalean.ML.RegularizedERM · Causalean/ML/Core/ERM.lean:44

structure IsERM reviewed

Causalean.ML

An empirical-risk minimizer is an admissible prediction rule whose finite-sample risk criterion is no larger than that of any other admissible rule. The criterion is the inverse-cardinality-scaled loss sum over a nonempty finite sample.

Definition (Lean source)

parameters

ι X Y :

Type*

Fintype ι

Nonempty ι

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

S :

ι → X × Y

hhat :

X → Y

fields

The minimizer belongs to the class.

mem :

hhat ∈ H.carrier

It minimizes empirical risk over the class.

isMin :

IsMinOn (fun h => empiricalRisk loss S h) H.carrier hhat

Causalean.ML.IsERM · Causalean/ML/Core/ERM.lean:55 · uses HypothesisClass , Loss

structure IsPopulationRiskMinimizer reviewed

Causalean.ML

A population-risk minimizer bundles the claim that a prediction rule belongs to the hypothesis class, that it has finite expected loss under the population measure, that every other rule admissible in the class also has finite expected loss, and that its population risk is no larger than that of any other rule in the class.

Definition (Lean source)

parameters

X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

H :

HypothesisClass X Y

loss :

Loss Y

P :

Measure (X × Y)

hstar :

X → Y

fields

The minimizer belongs to the class.

mem :

hstar ∈ H.carrier

The minimizer has finite expected loss.

finite_self :

HasFinitePopulationRisk loss P hstar

Every admissible competitor has finite expected loss.

finite_competitor :

∀ h ∈ H.carrier, HasFinitePopulationRisk loss P h

It minimizes population risk over the class.

isMin :

IsMinOn (fun h => populationRisk loss P h) H.carrier hstar

Causalean.ML.IsPopulationRiskMinimizer · Causalean/ML/Core/ERM.lean:67 · uses HypothesisClass , Loss

Losses 6 core · 7 supporting This file collects the elementary pointwise loss functions used throughout Causalean.ML: the squared loss for regression, and the sigmoid / softplus / score-space logistic loss for binary classification. ★ squaredLoss★ logisticScoreLoss★ bool01_true

Loss functions for the standalone ML module

This file collects the elementary pointwise loss functions used throughout Causalean.ML: the squared loss for regression, and the sigmoid / softplus / score-space logistic loss for binary classification. Everything here is causal-free real analysis; no probability or causal layer is imported.

def squaredLoss reviewed

Causalean.ML

Squared loss measures prediction error by squaring the difference between the observed label and the prediction.

Definition (Lean source)

def squaredLoss (ŷ y : ℝ) : ℝ := (y - ŷ) ^ 2

Causalean.ML.squaredLoss · Causalean/ML/Core/Losses.lean:19

def bool01 reviewed

Causalean.ML

Boolean labels are encoded as real zero-one outcomes.

Definition (Lean source)

def bool01 (b : Bool) : ℝ := if b then 1 else 0

Causalean.ML.bool01 · Causalean/ML/Core/Losses.lean:23

def sigmoid reviewed

Causalean.ML

The logistic sigmoid maps any real score to a probability-like number between zero and one.

Definition (Lean source)

noncomputable def sigmoid (t : ℝ) : ℝ := (1 + exp (-t))⁻¹

Causalean.ML.sigmoid · Causalean/ML/Core/Losses.lean:26

def softplus reviewed

Causalean.ML

Softplus is a smooth positive transformation used to write logistic losses in score space.

Definition (Lean source)

noncomputable def softplus (t : ℝ) : ℝ := log (1 + exp t)

Causalean.ML.softplus · Causalean/ML/Core/Losses.lean:30

def logisticScoreLoss reviewed

Causalean.ML

Logistic score loss is the binary cross-entropy loss written as a function of the raw prediction score.

Definition (Lean source)

noncomputable def logisticScoreLoss (y : Bool) (t : ℝ) : ℝ := softplus t - bool01 y * t

Causalean.ML.logisticScoreLoss · Causalean/ML/Core/Losses.lean:34

lemma bool01_true reviewed

Causalean.ML

A true Boolean label is encoded as the real number one.

Formal statement

conclusion

bool01 true = 1

Proof (Lean source)

@[simp] lemma bool01_true : bool01 true = 1 := rfl

Causalean.ML.bool01_true · Causalean/ML/Core/Losses.lean:39 · uses bool01

7 supporting declarations (lemmas, instances)

bool01_false lemma — A false Boolean label is encoded as zero.

conclusion

bool01 false = 0

Proof (Lean source)

@[simp] lemma bool01_false : bool01 false = 0 := rfl

Causalean.ML.bool01_false · Causalean/ML/Core/Losses.lean:42
bool01_nonneg lemma — The zero-one encoding of a Boolean label is always nonnegative.

hypotheses

b :

Bool

conclusion

0 ≤ bool01 b

Proof (Lean source)

lemma bool01_nonneg (b : Bool) : 0 ≤ bool01 b := by cases b <;> simp [bool01]

Causalean.ML.bool01_nonneg · Causalean/ML/Core/Losses.lean:45
bool01_le_one lemma — The zero-one encoding of a Boolean label is always at most one.

hypotheses

b :

Bool

conclusion

bool01 b ≤ 1

Proof (Lean source)

lemma bool01_le_one (b : Bool) : bool01 b ≤ 1 := by cases b <;> simp [bool01]

Causalean.ML.bool01_le_one · Causalean/ML/Core/Losses.lean:49
squaredLoss_nonneg lemma — Squared loss is always nonnegative.

hypotheses

ŷ y :

ℝ

conclusion

0 ≤ squaredLoss ŷ y

Proof (Lean source)

lemma squaredLoss_nonneg (ŷ y : ℝ) : 0 ≤ squaredLoss ŷ y := sq_nonneg _

Causalean.ML.squaredLoss_nonneg · Causalean/ML/Core/Losses.lean:53
sigmoid_pos lemma — The logistic sigmoid is strictly positive at every score.

hypotheses

t :

ℝ

conclusion

0 < sigmoid t

Proof (Lean source)

lemma sigmoid_pos (t : ℝ) : 0 < sigmoid t := by have : 0 < 1 + exp (-t) := by positivity exact inv_pos.mpr this

Causalean.ML.sigmoid_pos · Causalean/ML/Core/Losses.lean:56
sigmoid_lt_one lemma — The logistic sigmoid is strictly below one at every score.

hypotheses

t :

ℝ

conclusion

sigmoid t < 1

Proof (Lean source)

lemma sigmoid_lt_one (t : ℝ) : sigmoid t < 1 := by have hpos : (0 : ℝ) < exp (-t) := Real.exp_pos _ have h1 : (1 : ℝ) < 1 + exp (-t) := by linarith calc sigmoid t = (1 + exp (-t))⁻¹ := rfl _ < 1 := by rw [inv_lt_one_iff₀] right; exact h1

Causalean.ML.sigmoid_lt_one · Causalean/ML/Core/Losses.lean:61
softplus_pos lemma — Softplus is strictly positive at every score.

hypotheses

t :

ℝ

conclusion

0 < softplus t

Proof (Lean source)

lemma softplus_pos (t : ℝ) : 0 < softplus t := by have hpos : (0 : ℝ) < exp t := Real.exp_pos _ have h1 : (1 : ℝ) < 1 + exp t := by linarith exact Real.log_pos h1

Causalean.ML.softplus_pos · Causalean/ML/Core/Losses.lean:70

Bridge 2 core · 1 supporting The image of a Predictor under its prediction map is a HypothesisClass, and a *parametric* minimizer pushes forward to an *extensional* minimizer over that image class. ★ populationTarget_pushforward

Bridge between the parametric and extensional views

The image of a Predictor under its prediction map is a HypothesisClass, and a parametric minimizer pushes forward to an extensional minimizer over that image class. These two lemmas are the only glue between the two views of a method: properties stated in parameter space (convexity, regularization, optimization) transfer to the function-class statements (best-in-class, population target).

def imageClass reviewed

Causalean.ML

The hypothesis class realized by a predictor: the image of its admissible parameter set under the prediction map.

Definition (Lean source)

def imageClass {Θ X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) : HypothesisClass X Y where carrier := (fun θ => M.predict θ) '' M.paramSet measurable := by rintro h ⟨θ, hθ, rfl⟩ exact hmeas θ hθ

Causalean.ML.imageClass · Causalean/ML/Core/Bridge.lean:22 · uses HypothesisClass , Predictor

theorem populationTarget_pushforward reviewed

Causalean.ML

Population-target pushforward. For a predictor M with loss loss and population law P, suppose every admissible parameter's prediction function is measurable, the parameter θhat is itself admissible, every admissible parameter attains finite population risk, and θhat minimizes the population risk over the admissible parameter set. Then the predictor M.predict θhat is a population-risk minimizer over the hypothesis class realized by M's image: a parametric population-risk minimizer pushes forward to an extensional minimizer over the realized function class.

Formal statement

hypotheses

Θ X Y :

Type*

MeasurableSpace X

MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

P :

Measure (X × Y)

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

hmem :

θhat ∈ M.paramSet

hfinite :

∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)

h :

IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat

conclusion

IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem

Proof (Lean source)

theorem populationTarget_pushforward {Θ X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (P : Measure (X × Y)) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (hmem : θhat ∈ M.paramSet) (hfinite : ∀ θ ∈ M.paramSet, HasFinitePopulationRisk loss P (M.predict θ)) (h : IsMinOn (fun θ => populationRiskP M loss P θ) M.paramSet θhat) : IsPopulationRiskMinimizer (imageClass M hmeas) loss P (M.predict θhat) where mem := ⟨θhat, hmem, rfl⟩ finite_self := hfinite θhat hmem finite_competitor := by rintro g ⟨θ, hθ, rfl⟩ exact hfinite θ hθ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [populationRiskP] using (isMinOn_iff.mp h) θ hθ

Causalean.ML.populationTarget_pushforward · Causalean/ML/Core/Bridge.lean:46 · uses HasFinitePopulationRisk , IsPopulationRiskMinimizer , Loss , Predictor , imageClass , populationRiskP

1 supporting declaration (lemmas, instances)

isERMP_to_extensional theorem — A parametric empirical-risk minimizer pushes forward to an extensional empirical-risk minimizer over the realized hypothesis class.

hypotheses

ι Θ X Y :

Type*
Fintype ι
Nonempty ι
MeasurableSpace X
MeasurableSpace Y

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

hmeas :

∀ θ ∈ M.paramSet, Measurable (M.predict θ)

θhat :

Θ

h :

IsERMP (empiricalRiskP M loss S) M.paramSet θhat

conclusion

IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem

Proof (Lean source)

theorem isERMP_to_extensional {ι Θ X Y : Type*} [Fintype ι] [Nonempty ι] [MeasurableSpace X] [MeasurableSpace Y] (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (hmeas : ∀ θ ∈ M.paramSet, Measurable (M.predict θ)) {θhat : Θ} (h : IsERMP (empiricalRiskP M loss S) M.paramSet θhat) : IsERM (imageClass M hmeas) loss S (M.predict θhat) where mem := ⟨θhat, h.mem, rfl⟩ isMin := by rw [isMinOn_iff] rintro g ⟨θ, hθ, rfl⟩ simpa [empiricalRiskP] using (isMinOn_iff.mp h.isMin) θ hθ

Causalean.ML.isERMP_to_extensional · Causalean/ML/Core/Bridge.lean:32

Convex 2 core · 5 supporting Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. ★ exists_isMinOn_univ_of_coercive

Convex-analysis substrate for ERM

Reusable convexity, existence, first-order-optimality and subgradient facts that the convex methods (logistic regression, lasso, generic convex ERM) instantiate. This file is method-agnostic: it speaks only about an abstract objective on a real vector / inner-product / normed space.

theorem exists_isMinOn_univ_of_coercive reviewed

Causalean.ML

Existence via coercivity. On a proper normed real vector space, if the objective function is continuous and it tends to infinity along the cocompact filter, i.e. it is coercive — it grows without bound as the argument leaves every compact set, then a global minimizer of the objective over the whole space exists.

Formal statement

hypotheses

objective :

E → ℝ

hcont :

Continuous objective

hcoer :

Tendsto objective (cocompact E) atTop

conclusion

∃ a, IsMinOn objective univ a

Proof (Lean source)

theorem exists_isMinOn_univ_of_coercive {objective : E → ℝ} (hcont : Continuous objective) (hcoer : Tendsto objective (cocompact E) atTop) : ∃ a, IsMinOn objective univ a := by have _ : ProperSpace E := inferInstance obtain ⟨a, ha⟩ := hcont.exists_forall_le hcoer exact ⟨a, isMinOn_univ_iff.2 ha⟩

Causalean.ML.exists_isMinOn_univ_of_coercive · Causalean/ML/Core/Convex.lean:91

def SubgradientAt reviewed

Causalean.ML

g is a subgradient of f at x relative to s: the affine support inequality f x + ⟪g, y − x⟫ ≤ f y holds for all y ∈ s (and x ∈ s).

Definition (Lean source)

def SubgradientAt (f : E → ℝ) (s : Set E) (g x : E) : Prop := x ∈ s ∧ ∀ y ∈ s, f x + inner ℝ g (y - x) ≤ f y

Causalean.ML.SubgradientAt · Causalean/ML/Core/Convex.lean:121

5 supporting declarations (lemmas, instances)

empiricalRiskP_convexOn_of_loss_convex theorem — If every per-sample parameter loss is convex on Θset, so is the empirical risk of the predictor.

hypotheses

M :

Predictor Θ X Y

loss :

Loss Y

S :

ι → X × Y

Θset :

Set Θ

hconv :

Convex ℝ Θset

hloss :

∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)

conclusion

ConvexOn ℝ Θset (empiricalRiskP M loss S)

Proof (Lean source)

theorem empiricalRiskP_convexOn_of_loss_convex (M : Predictor Θ X Y) (loss : Loss Y) (S : ι → X × Y) (Θset : Set Θ) (hconv : Convex ℝ Θset) (hloss : ∀ i, ConvexOn ℝ Θset (fun θ => loss (M.predict θ (S i).1) (S i).2)) : ConvexOn ℝ Θset (empiricalRiskP M loss S) := by unfold empiricalRiskP empiricalRisk have hsum : ConvexOn ℝ Θset (fun θ => ∑ i, loss (M.predict θ (S i).1) (S i).2) := by classical have hfin : ∀ t : Finset ι, ConvexOn ℝ Θset (fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) := by intro t induction t using Finset.induction_on with | empty => simpa using (convexOn_const (𝕜 := ℝ) (E := Θ) (β := ℝ) (s := Θset) (0 : ℝ) hconv) | insert i t hi ht => have hadd := (hloss i).add ht have hfun : ((fun θ => loss (M.predict θ (S i).1) (S i).2) + fun θ => t.sum (fun i => loss (M.predict θ (S i).1) (S i).2)) = fun θ => (insert i t).sum (fun i => loss (M.predict θ (S i).1) (S i).2) := by funext θ simp [Finset.sum_insert hi] rwa [hfun] at hadd simpa using hfin univ simpa [smul_eq_mul] using hsum.smul (inv_nonneg.mpr (Nat.cast_nonneg (card ι)))

Causalean.ML.empiricalRiskP_convexOn_of_loss_convex · Causalean/ML/Core/Convex.lean:27
convexOn_comp_inner theorem — A convex scalar function precomposed with the linear score θ ↦ ⟪θ, x⟫ is convex. This is the workhorse turning convexity of a margin loss into convexity of the parameter objective.

hypotheses

φ :

ℝ → ℝ

hφ :

ConvexOn ℝ univ φ

x :

E

conclusion

ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x))

Proof (Lean source)

theorem convexOn_comp_inner {φ : ℝ → ℝ} (hφ : ConvexOn ℝ univ φ) (x : E) : ConvexOn ℝ univ (fun θ : E => φ (inner ℝ θ x)) := by simpa [Function.comp_def, innerSL_apply_apply, real_inner_comm] using hφ.comp_linearMap ((innerSL ℝ x).toLinearMap)

Causalean.ML.convexOn_comp_inner · Causalean/ML/Core/Convex.lean:64
exists_isMinOn_of_isCompact theorem — Existence of a minimizer on a nonempty compact set (Weierstrass).

hypotheses

objective :

Θ → ℝ

Θset :

Set Θ

hne :

Θset.Nonempty

hcompact :

IsCompact Θset

hcont :

ContinuousOn objective Θset

conclusion

∃ θhat ∈ Θset, IsMinOn objective Θset θhat

Proof (Lean source)

theorem exists_isMinOn_of_isCompact {objective : Θ → ℝ} {Θset : Set Θ} (hne : Θset.Nonempty) (hcompact : IsCompact Θset) (hcont : ContinuousOn objective Θset) : ∃ θhat ∈ Θset, IsMinOn objective Θset θhat := by exact hcompact.exists_isMinOn hne hcont

Causalean.ML.exists_isMinOn_of_isCompact · Causalean/ML/Core/Convex.lean:78
fderiv_eq_zero_of_isMinOn_univ theorem — First-order optimality on the whole space: at an unconstrained minimizer the Fréchet derivative vanishes.

hypotheses

f :

E → ℝ

f' :

E →L[ℝ] ℝ

a :

E

hmin :

IsMinOn f univ a

hderiv :

HasFDerivAt f f' a

conclusion

f' = 0

Proof (Lean source)

theorem fderiv_eq_zero_of_isMinOn_univ {f : E → ℝ} {f' : E →L[ℝ] ℝ} {a : E} (hmin : IsMinOn f univ a) (hderiv : HasFDerivAt f f' a) : f' = 0 := by exact (hmin.isLocalMin univ_mem).hasFDerivAt_eq_zero hderiv

Causalean.ML.fderiv_eq_zero_of_isMinOn_univ · Causalean/ML/Core/Convex.lean:109
subgradientAt_zero_iff_isMinOn theorem — Fermat's rule, subgradient form: 0 is a subgradient at x over s iff x minimizes f over s.

hypotheses

f :

E → ℝ

s :

Set E

x :

E

hx :

x ∈ s

conclusion

SubgradientAt f s 0 x ↔ IsMinOn f s x

Proof (Lean source)

theorem subgradientAt_zero_iff_isMinOn {f : E → ℝ} {s : Set E} {x : E} (hx : x ∈ s) : SubgradientAt f s 0 x ↔ IsMinOn f s x := by constructor · intro h exact isMinOn_iff.2 fun y hy => by have := h.2 y hy simpa [SubgradientAt, inner_zero_left] using this · intro hmin refine ⟨hx, ?_⟩ intro y hy simpa [SubgradientAt, inner_zero_left] using (isMinOn_iff.1 hmin y hy)

Causalean.ML.subgradientAt_zero_iff_isMinOn · Causalean/ML/Core/Convex.lean:126

PopulationTarget 2 core · 2 supporting This file collects reusable statements about what a population-risk minimizer recovers. ★ IsL2Projection★ square_loss_population_target_of_isL2Projection

Population-risk targets

This file collects reusable statements about what a population-risk minimizer recovers. populationRisk_eq_of_both_minimizers shows that any two minimizers attain the same risk, while populationRisk_minimizer_eq_target turns a unique target minimizer into equality of functions. For squared loss, IsL2Projection records the residual-orthogonality property of an L² projection, and square_loss_population_target_of_isL2Projection proves that such a projection minimizes squared population risk. The conditional-expectation bridge is isolated in ML/CausalApplication/RegressionBridge.lean, so this layer stays self-contained and causal-free.

def IsL2Projection reviewed

Causalean.ML

The residual of m is orthogonal to every (integrable, measurable) function of the covariate. This is the defining property of the L²-projection onto the σ-algebra generated by the covariate, i.e. of the regression function x ↦ E[Y ∣ X = x]. Measurability of the test function g is required because orthogonality of the residual is only meaningful for measurable functions of X (it is what links this to condExp; see ML/CausalApplication/RegressionBridge.lean).

Definition (Lean source)

def IsL2Projection (P : Measure (X × ℝ)) (m : X → ℝ) : Prop := ∀ g : X → ℝ, Measurable g → Integrable (fun z => (z.2 - m z.1) * g z.1) P → ∫ z, (z.2 - m z.1) * g z.1 ∂P = 0

Causalean.ML.IsL2Projection · Causalean/ML/Core/PopulationTarget.lean:47

theorem square_loss_population_target_of_isL2Projection reviewed

Causalean.ML

For a joint covariate–response law P and a competitor function h, if the residual of m is orthogonal to every function of the covariate, i.e. m is an L² projection onto functions of the covariate, m is measurable, the competitor h is measurable, m attains finite squared population risk, h attains finite squared population risk, and the cross term (Y − m(X))·(m(X) − h(X)) is integrable, then the squared population risk of m is at most that of h: m minimizes squared population risk against any such competitor.

Formal statement

hypotheses

P :

Measure (X × ℝ)

m :

X → ℝ

hm :

IsL2Projection P m

h :

X → ℝ

hm_meas :

Measurable m

hh_meas :

Measurable h

hint_m :

HasFinitePopulationRisk squaredLoss P m

hint_h :

HasFinitePopulationRisk squaredLoss P h

hcross :

Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P

conclusion

populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h

Proof (Lean source)

theorem square_loss_population_target_of_isL2Projection {P : Measure (X × ℝ)} {m : X → ℝ} (hm : IsL2Projection P m) (h : X → ℝ) (hm_meas : Measurable m) (hh_meas : Measurable h) (hint_m : HasFinitePopulationRisk squaredLoss P m) (hint_h : HasFinitePopulationRisk squaredLoss P h) (hcross : Integrable (fun z => (z.2 - m z.1) * (m z.1 - h z.1)) P) : populationRisk squaredLoss P m ≤ populationRisk squaredLoss P h := by have hint_m' : Integrable (fun z : X × ℝ => (z.2 - m z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_m have hint_h' : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss] using hint_h have hdiff : Integrable (fun z : X × ℝ => (z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) P := hint_h'.sub hint_m' have hsq_int : Integrable (fun z : X × ℝ => (m z.1 - h z.1) ^ 2) P := by have htmp : Integrable (fun z : X × ℝ => ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) - 2 * ((z.2 - m z.1) * (m z.1 - h z.1))) P := hdiff.sub (hcross.const_mul 2) convert htmp using 1 funext z ring have horth : ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P = 0 := hm (fun x => m x - h x) (hm_meas.sub hh_meas) hcross have hdiff_nonneg : 0 ≤ ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by calc 0 ≤ ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by exact integral_nonneg (fun z => sq_nonneg _) _ = 2 * ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P + ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by simp [horth] _ = ∫ z, 2 * ((z.2 - m z.1) * (m z.1 - h z.1)) + (m z.1 - h z.1) ^ 2 ∂P := by rw [integral_add] · rw [integral_const_mul] · exact hcross.const_mul 2 · exact hsq_int _ = ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by apply integral_congr_ae filter_upwards with z ring have hle : ∫ z, (z.2 - m z.1) ^ 2 ∂P ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P := by have hnonneg_sub : 0 ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P - ∫ z, (z.2 - m z.1) ^ 2 ∂P := by rw [← integral_sub hint_h' hint_m'] exact hdiff_nonneg linarith simpa [populationRisk, squaredLoss] using hle

Causalean.ML.square_loss_population_target_of_isL2Projection · Causalean/ML/Core/PopulationTarget.lean:57 · uses HasFinitePopulationRisk , IsL2Projection , populationRisk , squaredLoss

2 supporting declarations (lemmas, instances)

populationRisk_eq_of_both_minimizers theorem — Any two population-risk minimizers over the same class attain the same risk.

hypotheses

H :

HypothesisClass X Y

loss :

Loss Y

P :

Measure (X × Y)

h₁ h₂ :

X → Y

H1 :

IsPopulationRiskMinimizer H loss P h₁

H2 :

IsPopulationRiskMinimizer H loss P h₂

conclusion

populationRisk loss P h₁ = populationRisk loss P h₂

Proof (Lean source)

theorem populationRisk_eq_of_both_minimizers {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {h₁ h₂ : X → Y} (H1 : IsPopulationRiskMinimizer H loss P h₁) (H2 : IsPopulationRiskMinimizer H loss P h₂) : populationRisk loss P h₁ = populationRisk loss P h₂ := le_antisymm ((isMinOn_iff.mp H1.isMin) h₂ H2.mem) ((isMinOn_iff.mp H2.isMin) h₁ H1.mem)

Causalean.ML.populationRisk_eq_of_both_minimizers · Causalean/ML/Core/PopulationTarget.lean:28
populationRisk_minimizer_eq_target theorem — If a target is known to be the unique population-risk minimizer, every population-risk minimizer equals it.

hypotheses

H :

HypothesisClass X Y

loss :

Loss Y

P :

Measure (X × Y)

target hstar :

X → Y

hStar :

IsPopulationRiskMinimizer H loss P hstar

hTarget :

IsPopulationRiskMinimizer H loss P target

hUnique :

∀ h₁ h₂
if
IsPopulationRiskMinimizer H loss P h₁
and
IsPopulationRiskMinimizer H loss P h₂
then
h₁ = h₂

conclusion

hstar = target

Proof (Lean source)

theorem populationRisk_minimizer_eq_target {H : HypothesisClass X Y} {loss : Loss Y} {P : Measure (X × Y)} {target hstar : X → Y} (hStar : IsPopulationRiskMinimizer H loss P hstar) (hTarget : IsPopulationRiskMinimizer H loss P target) (hUnique : ∀ h₁ h₂, IsPopulationRiskMinimizer H loss P h₁ → IsPopulationRiskMinimizer H loss P h₂ → h₁ = h₂) : hstar = target := hUnique hstar target hStar hTarget

Causalean.ML.populationRisk_minimizer_eq_target · Causalean/ML/Core/PopulationTarget.lean:36

Rate 2 core · 2 supporting The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions). ★ isLittleOp_mul_quarter★ AchievesL2Rate

Learning-rate abstraction and rate algebra

The causal-free common currency between the method folders (which prove per-method L²-estimation rates) and ML/CausalApplication (which assembles them to discharge DML's nuisance-rate conditions).

* AchievesL2Rate ĥ h⋆ P rₙ μ — every L² seminorm of the estimation error is finite, and its real-number conversion is O_p(rₙ) under the experiment law. * generic probabilistic stochastic-order facts: an o_p(rₙ) with rₙ ≤ 1 is o_p(1); a product of two o_p(n^{-1/4}) is o_p(n^{-1/2}); and an O_p(n^{-1/2}) rate is o_p(n^{-1/4}) (turning a method's root-n IsBigOp into the o_p(n^{-1/4}) the DML side consumes).

theorem isLittleOp_mul_quarter reviewed

Causalean.ML

The n^{-1/4} product rule. If the sequence Xn is o_p(n^{-1/4}) and the sequence Yn is o_p(n^{-1/4}) under the probability law μ, then their pointwise product Xn·Yn is o_p(n^{-1/2}) — the DML product-rate condition from per-nuisance n^{-1/4} rates.

Formal statement

hypotheses

hX :

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

hY :

IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

conclusion

IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_mul_quarter (hX : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) (hY : IsLittleOp Yn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) : IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε let δ : ℝ := Real.sqrt ε have hδpos : 0 < δ := Real.sqrt_pos.2 hε have hδsq : δ * δ = ε := by simpa [δ, pow_two] using Real.sq_sqrt (le_of_lt hε) let A : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) < |Xn n ω * Yn n ω|} have hAt : Tendsto (fun n => μ (A n)) atTop (𝓝 0) := by simpa [A, δ] using hX δ hδpos have hBt : Tendsto (fun n => μ (B n)) atTop (𝓝 0) := by simpa [B, δ] using hY δ hδpos have hsum : Tendsto (fun n => μ (A n) + μ (B n)) atTop (𝓝 0) := by simpa using hAt.add hBt refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hsum (Eventually.of_forall fun n => zero_le) ?_ filter_upwards [eventually_ge_atTop 1] with n hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn have hrate_nonneg : 0 ≤ (n : ℝ) ^ (-(1 / 4 : ℝ)) := Real.rpow_nonneg (Nat.cast_nonneg n) _ have hrate_prod : (n : ℝ) ^ (-(1 / 4 : ℝ)) * (n : ℝ) ^ (-(1 / 4 : ℝ)) = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← Real.rpow_add hnpos] congr 1 norm_num have hpoint : μ (C n) ≤ μ (A n) + μ (B n) := by have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := le_of_not_gt hnotB have hbound_nonneg : 0 ≤ δ * (n : ℝ) ^ (-(1 / 4 : ℝ)) := mul_nonneg (le_of_lt hδpos) hrate_nonneg have hprod : |Xn n ω * Yn n ω| ≤ ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ ≤ (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) * (δ * (n : ℝ) ^ (-(1 / 4 : ℝ))) := mul_le_mul hXle hYle (abs_nonneg _) hbound_nonneg _ = ε * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [mul_mul_mul_comm, hδsq, hrate_prod] exact not_lt_of_ge hprod hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) simpa [C] using hpoint

Causalean.ML.isLittleOp_mul_quarter · Causalean/ML/Core/Rate.lean:43 · uses IsLittleOp

def AchievesL2Rate reviewed

Causalean.ML

The L² estimation error has a finite seminorm at every sample size and experiment outcome, and that finite seminorm is stochastically bounded at the supplied rate under the experiment law. The L² seminorm is computed using the covariate marginal of the joint law, so the real-valued stochastic-order claim never comes from converting an infinite extended norm to zero.

Definition (Lean source)

def AchievesL2Rate {X : Type*} [MeasurableSpace X] (hhat : ℕ → Ω → (X → ℝ)) (hstar : X → ℝ) (P : Measure (X × ℝ)) (rn : ℕ → ℝ) (μ : Measure Ω) : Prop := (∀ n ω, eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst) ≠ ⊤) ∧ IsBigOp (fun n ω => (eLpNorm (fun x => hhat n ω x - hstar x) 2 (P.map fst)).toReal) rn μ

Causalean.ML.AchievesL2Rate · Causalean/ML/Core/Rate.lean:196

2 supporting declarations (lemmas, instances)

isLittleOp_one_of_le_one theorem — Rate weakening: an o_p(rn) sequence with rn ≤ 1 is o_p(1).

hypotheses

rn :

ℕ → ℝ

hr :

∀ n, rn n ≤ 1

h :

IsLittleOp Xn rn μ

conclusion

IsLittleOp Xn (fun _ => 1) μ

Proof (Lean source)

theorem isLittleOp_one_of_le_one {rn : ℕ → ℝ} (hr : ∀ n, rn n ≤ 1) (h : IsLittleOp Xn rn μ) : IsLittleOp Xn (fun _ => 1) μ := by intro ε hε have hlim : Tendsto (fun n => μ {ω | ε * rn n < |Xn n ω|}) atTop (𝓝 0) := h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hlim (fun n => zero_le) ?_ intro n apply measure_mono intro ω hω have hmul : ε * rn n ≤ ε * 1 := mul_le_mul_of_nonneg_left (hr n) (le_of_lt hε) exact lt_of_le_of_lt hmul (by simpa using hω)

Causalean.ML.isLittleOp_one_of_le_one · Causalean/ML/Core/Rate.lean:29
isLittleOp_quarter_of_isBigOp_sqrt theorem — An O_p(n^{-1/2}) (root-n) rate is o_p(n^{-1/4}): a method's root-n estimation rate clears the DML o_p(n^{-1/4}) bar.

hypotheses

h :

IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ

conclusion

IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ

Proof (Lean source)

theorem isLittleOp_quarter_of_isBigOp_sqrt (h : IsBigOp Xn (fun n => (sqrt (n : ℝ))⁻¹) μ) : IsLittleOp Xn (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 2 have hαpos : 0 < α := by dsimp [α] linarith rcases h α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | M * (sqrt (n : ℝ))⁻¹ < |Xn n ω|} have hlimB : limsup (fun n => μ (B n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [B] at hω ⊢ have hrate_nonneg : 0 ≤ (sqrt (n : ℝ))⁻¹ := inv_nonneg.mpr (Real.sqrt_nonneg _) exact lt_of_le_of_lt (mul_le_mul_of_nonneg_right hM0le hrate_nonneg) hω have hα_lt_delta : ofReal α < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimB hα_lt_delta) have hthreshold : ∀ᶠ n : ℕ in atTop, M * (sqrt (n : ℝ))⁻¹ ≤ ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by have ht : Tendsto (fun n : ℕ => (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by have hp : Tendsto (fun x : ℝ => x ^ (-(1 / 4 : ℝ))) atTop (𝓝 0) := by exact tendsto_rpow_neg_atTop (by norm_num : (0 : ℝ) < (1 / 4 : ℝ)) simpa using (Tendsto.const_mul (M / ε) (hp.comp tendsto_natCast_atTop_atTop)) have hevent_abs : ∀ᶠ n : ℕ in atTop, |(M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ))| < 1 := by have hnear := (Metric.tendsto_nhds.mp ht) 1 (by norm_num : (0 : ℝ) < (1 : ℝ)) simpa [Real.dist_eq, abs_mul, abs_div] using hnear filter_upwards [hevent_abs, eventually_ge_atTop 1] with n hnabs hn_ge have hnsmall : (M / ε) * (n : ℝ) ^ (-(1 / 4 : ℝ)) < 1 := (abs_lt.mp hnabs).2 have hnpos : 0 < (n : ℝ) := by exact_mod_cast hn_ge let q : ℝ := (n : ℝ) ^ (-(1 / 4 : ℝ)) have hqpos : 0 < q := by dsimp [q] exact Real.rpow_pos_of_pos hnpos _ have hinv_eq : (sqrt (n : ℝ))⁻¹ = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [Real.sqrt_eq_rpow] rw [← Real.rpow_neg (le_of_lt hnpos)] have hpow_add : q * q = (n : ℝ) ^ (-(1 / 2 : ℝ)) := by dsimp [q] rw [← Real.rpow_add hnpos] congr 1 norm_num have hmul : (M / ε * q) * (ε * q) ≤ 1 * (ε * q) := by exact mul_le_mul_of_nonneg_right (le_of_lt hnsmall) (le_of_lt (mul_pos hε hqpos)) have hleft : (M / ε * q) * (ε * q) = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [← hpow_add] field_simp [hε.ne'] calc M * (sqrt (n : ℝ))⁻¹ = M * (n : ℝ) ^ (-(1 / 2 : ℝ)) := by rw [hinv_eq] _ = (M / ε * q) * (ε * q) := by rw [hleft] _ ≤ 1 * (ε * q) := hmul _ = ε * (n : ℝ) ^ (-(1 / 4 : ℝ)) := by simp [q] filter_upwards [hBevent, hthreshold] with n hBn hthr have hsubset : A n ⊆ B n := by intro ω hω dsimp [A, B] at hω ⊢ exact lt_of_le_of_lt hthr hω have heq : {ω | ε * (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) n < |Xn n ω|} = A n := by ext ω simp [A] rw [heq] exact le_of_lt (lt_of_le_of_lt (measure_mono hsubset) hBn)

Causalean.ML.isLittleOp_quarter_of_isBigOp_sqrt · Causalean/ML/Core/Rate.lean:106