Solution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem classical_carleson' line 11 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: ClassicalCarleson

   Proof uses: classical_carleson

   Distinct definitions of this name: Challenge.lean:10 (same statement text; different proof or body). Qualify references as classical_carleson'@path.

2. theorem metric_carleson'' line 13 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: MetricSpaceCarleson

   Proof uses: metric_carleson

   Distinct definitions of this name: Challenge.lean:12 (same statement text; different proof or body). Qualify references as metric_carleson''@path.

3. theorem linearized_metric_carleson' line 15 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: LinearizedMetricCarleson

   Proof uses: linearized_metric_carleson

   Distinct definitions of this name: Challenge.lean:14 (same statement text; different proof or body). Qualify references as linearized_metric_carleson'@path.